There are a lot of results about conditional lower bounds: "If this problem is at least this hard, that other problem must be at least that hard." But now a widely used assumption was proven wrong, and an entire house of cards collapsed.
It feels like that particular research direction is now a dead end, until we can figure out a way of proving conditional bounds that is robust against technicalities. We would like to prove something like "If this problem is essentially at least this hard, that other problem must be essentially at least that hard." If the conditional bound depends on the assumption that the first problem requires at least n^2 time but somebody comes up with an O(n^1.9992) time algorithm, a slightly weaker conditional bound would still remain.
This is the most negative possible take on the most positive possible kind of result in CS.
To see just how unduly negative it is, imagine how different your response would have been had the exact same result been reported in a paper by exclusively human authors. Would you have likewise accused them of creating a research "dead end"?
EDIT: Changed "by, e.g., Ryan Williams" to "by exclusively human authors". Without having checked the authors, who include Ryan's wife and frequent collaborator Virginia, I had reached for a big name in the field purely as an example of a human who might well have made this breakthrough on their own.
Conditional lower bounds are a way of building understanding of the essential difficulty of specific computational problems. But if AI can now routinely generate marginal improvements, conditional bounds based on unproven assumptions become a waste of effort.
This is mostly due to how mathematics works. Ideally, we would like to prove something like "if problem A is essentially this difficult, problem B is essentially that difficult". But what we actually prove is more like "if (specific formulation of the difficulty of problem A), then (specific formulation of the difficulty of problem B)".
But those specific formulations become fixed targets for the AI to attack. If it manages to break the specific assumption, for example by creating an O(n^1.9998) time algorithm that is for all intents and purposes worse than a naive O(n^2) time algorithm, the conditional result becomes void. We could try to salvage the result with a different formulation, but that again becomes a fixed target.
This is essentially Goodhart's Law. We measure improvement with highly precise metrics, while we are actually interested in qualitative understanding.
EDIT: If theorems and proofs become cheap, marginal improvements are no longer interesting. Qualitatively better algorithms or unconditional lower bounds would be actual contributions. As would be a specific formulation of a conditional result that is robust against technical improvements made by AI targeting that specific formulation.
i feel like you are arguing there is -- even in the narrow utility of PROOFS -- there is a goodness in being an ostrich with its head in the sand. If that's true, people can still be that ostrich and pretend the bound is now n^1.9 or something.
The actual conditional result was "if problem A is essentially this difficult, problem B is essentially that difficult". A specific formulation of it was proven, but it depended on a specific assumption that was just shown false. But the general result is still probably valid, because the general assumption holds. But there may be no point in going through the effort of proving another specific formulation, when the automatic theorem factory could just come up with another technical improvement targeting that formulation.
I started in theoretical computer science, but I quickly drifted to more applied areas, because I was annoyed with how often theoreticians would confuse the map for the territory. But if AI can now do that much more efficiently than any human, perhaps theoreticians will have to rethink how much they should focus on specific provable statements.
This is the part of your reply that I find the most compelling. If such results can be produced "cheaply", then yes, it becomes less interesting for humans to devote their own time and energy to pursuing them. But while that would be bad news for mathematicians, I don't hold that to be a negative thing on its face. (I'm not sure that you do either, but it's a commonly held view and consistent with your words so far.) Fundamentally, that's because I don't think mathematicians have a right to do mathematics research for a living any more than buggy whip manufacturers have a right to make buggy whips for a living.
On the (to my mind, secondary) question of whether "small"/"technical" advances in algorithms will now become cheap: I don't think this will happen in any case. Unlike most applications of Goodhart's Law, which involve exploiting something trivial like line counts or git commits, I think improving a well-known problem's asymptotic complexity is sufficiently "meaty" that it will never be cheaply automated. Even if some theorem is discovered in future that "automates" optimal algorithm creation for a wide range of problems (imagine something like a turbocharged Courcelle's Theorem), I'm certain there will always be problems for which we don't know the answer.
As a non-mathematician who sometimes works on mathematical problems, I find this really puzzling. Why aren't mathematicians excited about the frontiers being unlocked by AI? The ability to discover more of the mathematical universe more readily?
I want lower energy bills, lower rent, better understanding of health etc. more than I want theorems.
The value of LLM is not "Ha curious look what it can do". It's not entertainment.
These efforts aren't mutually exclusive. I hate to be snide, but a lot of people would criticize you for being a mathematician because they want lower energy bills, lower rent, better understanding of health etc
And yes, nobody is that excited about vatsachak's mathematician-ism. it's just a thing he do. And now it's just a thing AI do.
I’m personally pretty excited by the results coming from these labs, but trying to dismiss the capital allocation objection with “but what about” is really silly.
Edit: I'm fine saying we're spending too much money on AI, in fact I agree, but "theorems" are not the only output of these companies. It's almost definitely not going to be worth the expenditure, but the benefits are not going to be only lean proofs
For the mathematicians who still are in academia: I guess because the competition for research positions (in particular permanent ones) is already insane; they probably feel that AI makes this kind of competition even worse.
Well, I wouldn't generalize based off of the thread OP (and people on social media, including me). I think a lot of us are very excited! Most of my collaborators are, including myself.
There's a lot of simultaneous social change that's accompanying these tools, not all of which is positive. Agonized screaming is pretty loud, relatively speaking to the rest of the conversation.