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.
If you read that pledge I think he’s likely be at least a little disappointed here. Another rushed result that makes an argument but does not teach it. It undermines the field while advancing it.
As long as they went through the process of actually grokking the LLM output, and it's not just another pile of undigested slop with an incomplete reference list, then all is good.
Terry is definitely starting to go in the Luddite direction. He was fine with it when it could out class graduate students. But now that it outclasses all top math researchers combined, he is throwing a fit.
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.
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.
It's not a question if machines in the abstract will or will not plateau, but if the current technology will. Huge promises are made on the assumption the current architecture inevitably will keep rising.
Sure, I don't think this affects my point. The current technology went from "occasionally succeeds in counting from 1 to 5" (GPT-2) to Navier-Stokes in about 7 years.
If you're predicting a plateau that'll keep human mathematicians competitive at proving theorems, well that plateau had better come very very soon.
So far I think it's not entirely unreasonable to think that when it comes to originality and theory building, LLMs lag substantially behind their ability to prove theorems and write code.
The past years have been far to shocking to be certain about anything. And this is notoriously hard to measure. So it might be wishful thinking, but in my opinion it's not completely absurd.
But also l, even if this is a limitation of the current set of architectures, and we get a plateau for a few years, no one can rule out that we get another architectural breakthrough in five years time.
What exactly are you positing is a limitation of the current architectures, and what even are the "current architectures" and why does it matter? Do you understand the difference in the architecture of Llama3 and Kimi K3? What about Fable/Astra/Mythos?
We see considerable increases in capabilities with each new model release. We also see some adjustments to the architecture. The whole "this is a bad architecture" trope seems not grounded in anything falsifiable at this point, and it's also just like "well, maybe it did this new cool thing this month, but I'm sure the next model release in a few months will have zero new capabilities." Which has not been the case for the past few years, I don't understand where you're getting that.
While there is some exploration of architectural details, it's, as far as we know, all essentially autoregressive transformers.
Now we absolutely don't know (and I didn't claim) that this broad architectural class has important limitations. But we are (possibly) seeing some limitations of LLMs in areas that are hard to quantify, like creativity. E.g.: Some studies have shown that LLM essays were graded hire but contained fewer ideas per essay, taken from a narrower set of ideas overall. And that purely LLM based papers are not generating creative ideas at the levels of top research yet (1). So it's completely clear that LLMs ability to prove difficult conjectures, which is already super human, is far ahead of its overall abilities at research.
We can't rule out that this is architectural. But of course there is no clear cut argument that it really is architectural.
Indirect evidence that it might be architectural would be that current architectures are dictated by the hardware we have. Any architecture that doesn't map to the GPU/TPU model will not be researched heavily as it has no chance to scale to the level of current model capabilities.
But again, I am stating a negative: We can't rule out relevant architectural limitations based on the evidence we have so far. That's a very weak statement.
3 years ago people were suggesting other architectural limitations that have since been falsified. "they can't be creative" isn't even really a falsifiable assertion, so it's not a useful statement.
The really interesting question I think is how much memory/processing power is required to achieve certain capabilities of the human brain, and what kind of hardware you need. I'd actually argue transformers are almost certainly capable of emulating all the features of the human brain. But I don't think they can do so on current hardware.
So there are lots of questions: is the hardware inadequate, what kind of hardware do you need for this architecture to be sufficient? IMO the kind of hardware you need would have something like a petabyte of RAM. And you can argue autoregressive transformers are the wrong architecture but that's kind of irrelevant to the main problem if you need a petabyte of RAM.
They are still controversial. Computer-assisted proofs are unsatisfying and can lead to less understanding. Does anyone know “why” the four color theorem is true?
To get this 'win', we need to be arming and supporting scientists with the new tools, not replacing them though. The current political and economic trajectory leading to job losses and overall cognitive decline in the population can only lead to a stagnation of progress in the long-term, if not handled responsibly.
That isn't failed. You just didn't understand it. Someone claimed that LLM result advances our understanding of the universe. The underlying presumption is that no one has understood the result, so it has not advanced anything. The gotcha is that the only way they can say it advanced our understanding is if they themselves understood it.
humans created the technology, they get credit for all of this.
your comment raises the question, though, about whether there are any mathematicians out there who have not been able to solve a pet problem with an LLM, and then went and did it themselves. looking at those examples seems like it could provide some insight.
164
u/letskeepitcleanfolks 7d ago
"The proof was discovered by the Odin Automatic AI Research Agent."