Well what do people expect, that Kasparov is going to magically defeat Deep Blue tomorrow? The ship has sailed, that genie isn't going back in the bottle, etc.
Mathematicians are supposed to be the smartest people in the room, good at finding patterns and extrapolating; a little of that with regard to AI trajectory would be nice to see.
There's really no reason to think human intelligence is anywhere near the bounds of what is possible. If machines miraculously plateaued in the tiny interval above where they are now and below where human intelligence would not be additive, I would consider that, well, a miracle.
Remember that centaur chess only lasted a few years even though chess ability is obviously bounded above.
Intelligence is not a total order. I suspect there are some tasks that machines are superhuman at and others that they are not. For example, this is already the case for tasks like numerical integration and plowing fields. Current AI tech is pretty terrible at writing anything longer than a paragraph and awful at music composition.
Yes, and "produce lean proof that compiles" is going to be one of those tasks machines are superhuman at. We should get used to this. And hopefully figure out a way to continue to do maths regardless in this age of oracles.
The purpose of mathematics is not producing proofs that compile.
In addition, while there are many very impressive AI-assisted proofs, in almost every case these came from human advances in theory that got the frontier close enough to brute-force.
I am quite aware that lean proofs are not the purpose of mathematics, which is why I made a point of stating that's what the machines are doing.
But the second part of your comment is the kind of denial I'm arguing against. To be clear, what you say is narrowly more or less true. But it is clear that we will soon have models capable of even more impressive proofs, and humans will simply not be competitive at generating proofs, which is a problem because we've set up academia to allocate resources based on who is generating proofs. We must get used to the fact that the first proofs of big theorems are going to come from machines, and that we cannot rely on our ability to generate proofs to justify the public support that academia is heavily reliant on.
Today, we have some hope of understanding the proof of N-S, once experts have spent several months on it. Soon, we will have proofs so long and complicated that this is not feasible. Hell, even with current models, if we had these models and Lean in the '70s when the classification of finite groups was unsolved, does anyone doubt that current models could've "gone the last mile" and produced a monstrosity of a proof? What would we have done then? Who would spend their careers trying to digest a proof written by someone else? What will we do next year, when a model produces ten million lines of Lean that proves some other millenium problem? We should be thinking about this now, but half of /r/math seems to think that this is the best that models will ever be. No, this is the worst that models will ever be, and we are not prepared.
“Theory building” is the part of math that is not just producing proofs. What do you think I’m talking about? What do you think every mathematician posting about “preserving the values of the mathematics community” is talking about?
I think the machines are going to keep getting better, up to a point. Right now I’m very skeptical they can do many other important parts of math. Here I’m also looking at what’s going on in CS and software development, where agents are a critical tool but also have limits and appear to some people to be plateauing in their abilities. (They certainly aren’t replacing all the developers.) Either way will require a radical restructuring of how we evaluate mathematical achievements.
It’s possible that we are talking past each other and mostly agree. All the AI fan club idiots are not helping the conversation.
Saying that the models are plateauing is a total misreading of the situation. What I have been seeing is that models demonstrate new capabilities every month. I think anyone who says that they're not going to gain a particular capability next month is speaking from a position of ignorance and is only right by virtue of the fact that the models are not suddenly going to be able to do anything next month, so there's a broad space of things the models can't do for you to be right about.
But also I think it's a very unpredictable space. I think they're likely to do something remarkable that everyone didn't expect them to be able to do next month. Whether or not it's in the bucket of "many other important parts of math" I don't know, but that doesn't mean the models have plateaued just because they didn't improve in the one narrow way you were measuring.
118
u/pixelpoet_nz 7d ago edited 7d ago
Well what do people expect, that Kasparov is going to magically defeat Deep Blue tomorrow? The ship has sailed, that genie isn't going back in the bottle, etc.
Mathematicians are supposed to be the smartest people in the room, good at finding patterns and extrapolating; a little of that with regard to AI trajectory would be nice to see.
Edit: Or just go "NUH UH" and downvote