I completely agree with him here. Pure mathematics has beauty because it comes from the human mind. Automation disturbs that beauty. I don’t want to know whether P=NP, I want to meet the person who discovers the answer by themselves and learn from them.
I do want to know. If AI figures it out, we can start from there and trace back the steps. Understanding the solution starting with the complete proof is much easier. No mathematician would throw away all the work of great and long dead mathematicians because of the beauty of figuring things out. You just go figure out the next unsolved thing.
Understanding the solution starting with the complete proof is much easier.
But that's what the thread is about: the solution is not the (most) valuable output from the research process. Instead it's the new mathematical tools and theories that emerge from our many failed and aborted attempts at a solution.
Okay, but do you throw away everything Gauss did and figure it out yourself from a state of ignorance because you might discover awesome tools along the way? How is standing on the shoulders of Gauss different from standing on the shoulders of a super smart AI? If you want the tools and theorems, read the reasoning logs and ask the AI what discoveries came up along the way. If the AI is indeed on that level, it will provide that which you claim is lost in the process.
do you throw away everything Gauss did and figure it out yourself from a state of ignorance because you might discover awesome tools along the way?
No[1]? We're talking about cutting edge research here, which cannot yet be solved with the current set of tools.
You have to stand on the shoulder of giants to build the next crop of tools and research that will allows us to tackle them.
How is standing on the shoulders of Gauss different from standing on the shoulders of a super smart AI?
Have you read the thread? Terence Tao has outlined it pretty clearly IMO: letting an AI run wild and come back with a more-or-less blackbox "yes/no" inherently reduces the paths to a solution we might explore, and thus reduce the possibility of uncovering new and useful tools along the way. Furthermore it is wasted energy to try and reverse-engineer the process from the solution.
In fact he is (potentially) defending a mixed approach, with a human in the loop augmented by LLMs.
EDIT
[1]: Actually maybe, sometimes... Calculus did not start off with the delta-epsilon definition, but we went back and tried to define it more rigorously by discarding the infinitesimal approach.
From my understanding, Bourbakism also helped create "awesome tools" in set theory through their approach to redefine all of mathematics in it.
How is standing on the shoulders of Gauss different from standing on the shoulders of a super smart AI? If you want the tools and theorems, read the reasoning logs and ask the AI what discoveries came up along the way.
This is addressed in the link, and is the main worry. It's not the LLM usage per se, but how it's gated and controlled.
But there is now a scenario in which an autonomous AI harness, backed by an enormous amount of computational resources, performs this entire iteration internally, and ends up producing the final ansatz, and thence the solution to the Navier-Stokes regularity problem, while the AI company running the harness keeps the process to arrive at that ansatz almost completely out of public view. Technically, one of the most prominent open problems in mathematics would now be solved; but there would be almost no value added to mathematics as a consequence.
What's the deal with this recurring "AI is just like humans, prove me wrong" thing? Must at least one comment thread rehash it every week so it stays in the context window?
Understanding the solution starting with the complete proof is much easier.
The unstated thing here is that the proof needs to be understandable; a claimed proof that cannot be understood may as well not exist. Furthermore, there needs to be trust that the understood proof is correct.
Mathematics is built on trust in other mathematicians. As you say in your other comments, we readily rely on the work of Gauss, Reimann, Euler, et. al., as we have a widely-held trust that their proofs are correct. We have this trust because we have a long history of studying and understanding their proofs and results. Their work is known to be good.
AI work is not known to be good. Producing a proof is one step of many, and a mere proof is almost never sufficient. We actually have a recent human example of exactly this circumstance: Inter-universal Teichmüller theory. Years have been given to the debate over IUT. AI will almost certainly create more of these sorts of debates, given that:
there will be a lot of claimed AI proofs
many of these proofs will be long / difficult
AI's predilection for hallucination
scarce human mathematician labor in reading, understanding, and communicating the worthwhile parts of these proofs
You just go figure out the next unsolved thing.
There is also the issue of finding "the next unsolved thing"; typically, it is research that produces more research questions. In a future where AI performs a significant portion of mathematics research, we lose the opportunity to find new research opportunities.
For my thesis at university, I wrote an evolutionary algorithm that generated algorithms to (hopefully optimally) solve a certain graph problem. The evolutionary algorithm kept optimizing into bugs in my code, exploiting loopholes where I forgot checks and limits. It took multiple iterations and fixes until it stopped optimizing into bugs and coming up with impossibly good algorithms. AI does the same on steroids. It might indeed become nearly impossible to ascertain that AI didn't exploit the tooling to achieve the proof if the complexity involved is large.
The funny thing: In the end, the best algorithm the evolutionary algorithm found was exactly the same one I found by hand. But I couldn't construct a proof of optimality. I wonder if someone has come up with it in the meantime.
… and the fact that finding another bug in Lean might be easier than the problem, and the fact that LLMs are clearly overtrained to exploit bugs…
On the other hand, maybe if the proof is translatable into enough automatic checkers, it could be accepted.
the worthwhile parts of these proofs
This is the really important part: the tradition is to count proofs because this is a way to keep score, but the real question is whether a proof moves understanding forward or consists purely of pointless slog. Humans also do proofs out of slog, but generally humans figure out things in the process and smplify. LLMs don't get tired in the same way as humans, so they might succeed with slog that explains nothing but technically speaking proves the original statement as written.
Zero-knowledge proofs don't need to be cryptographically sound to be useless.
Of course, maybe I was not clear in my statement. The point is not that I want to figure it myself. The point is that I enjoy reading a proof discovered by a human because it was discovered by a human. It’s the wonder for the capability of the human mind that inspires. Reading a machine generated proof would be not entertaining for me. Of course knowing the result may be useful. But not entertaining or inspiring like good math can be. But I suppose that’s just a matter of personal taste.
There was a fantastic post by David Bessis previousshared here that seems of revelance.
Quoted:
Let me emphasize that this is the same exact issue as in research. Problem solving is just a means to an end. The core payout of pure mathematics is the neuroplastic elevation of our worldview, and we can’t get there by copy-pasting the result.
To me, this might be the most striking aspect of the current moment. For all the flex and fury, the AI labs are barely engaging with mathematics itself, its core problems and significance. Which is entirely normal, since this is none of their business.
As Carl Jacobi once put it, “the object of mathematics is the honor of the human spirit.”
gignico | 13 days ago
I completely agree with him here. Pure mathematics has beauty because it comes from the human mind. Automation disturbs that beauty. I don’t want to know whether P=NP, I want to meet the person who discovers the answer by themselves and learn from them.
BenjaminRi | 13 days ago
I do want to know. If AI figures it out, we can start from there and trace back the steps. Understanding the solution starting with the complete proof is much easier. No mathematician would throw away all the work of great and long dead mathematicians because of the beauty of figuring things out. You just go figure out the next unsolved thing.
Ambroisie | 13 days ago
But that's what the thread is about: the solution is not the (most) valuable output from the research process. Instead it's the new mathematical tools and theories that emerge from our many failed and aborted attempts at a solution.
kolja | 13 days ago
The LLM mindset. As long as I can get there fast, I don't care if it's the right direction.
BenjaminRi | 13 days ago
Okay, but do you throw away everything Gauss did and figure it out yourself from a state of ignorance because you might discover awesome tools along the way? How is standing on the shoulders of Gauss different from standing on the shoulders of a super smart AI? If you want the tools and theorems, read the reasoning logs and ask the AI what discoveries came up along the way. If the AI is indeed on that level, it will provide that which you claim is lost in the process.
Ambroisie | 12 days ago
No[1]? We're talking about cutting edge research here, which cannot yet be solved with the current set of tools.
You have to stand on the shoulder of giants to build the next crop of tools and research that will allows us to tackle them.
Have you read the thread? Terence Tao has outlined it pretty clearly IMO: letting an AI run wild and come back with a more-or-less blackbox "yes/no" inherently reduces the paths to a solution we might explore, and thus reduce the possibility of uncovering new and useful tools along the way. Furthermore it is wasted energy to try and reverse-engineer the process from the solution.
In fact he is (potentially) defending a mixed approach, with a human in the loop augmented by LLMs.
EDIT
[1]: Actually maybe, sometimes... Calculus did not start off with the delta-epsilon definition, but we went back and tried to define it more rigorously by discarding the infinitesimal approach.
From my understanding, Bourbakism also helped create "awesome tools" in set theory through their approach to redefine all of mathematics in it.
psafont | 12 days ago
This is addressed in the link, and is the main worry. It's not the LLM usage per se, but how it's gated and controlled.
tentacloids | 13 days ago
What's the deal with this recurring "AI is just like humans, prove me wrong" thing? Must at least one comment thread rehash it every week so it stays in the context window?
BenjaminRi | 12 days ago
I never said this and I reject this characterization of my point above.
tentacloids | 12 days ago
If you insist! Maybe this thread will turn out different this time.
pretzel | 12 days ago
The unstated thing here is that the proof needs to be understandable; a claimed proof that cannot be understood may as well not exist. Furthermore, there needs to be trust that the understood proof is correct.
Mathematics is built on trust in other mathematicians. As you say in your other comments, we readily rely on the work of Gauss, Reimann, Euler, et. al., as we have a widely-held trust that their proofs are correct. We have this trust because we have a long history of studying and understanding their proofs and results. Their work is known to be good.
AI work is not known to be good. Producing a proof is one step of many, and a mere proof is almost never sufficient. We actually have a recent human example of exactly this circumstance: Inter-universal Teichmüller theory. Years have been given to the debate over IUT. AI will almost certainly create more of these sorts of debates, given that:
There is also the issue of finding "the next unsolved thing"; typically, it is research that produces more research questions. In a future where AI performs a significant portion of mathematics research, we lose the opportunity to find new research opportunities.
BenjaminRi | 12 days ago
For my thesis at university, I wrote an evolutionary algorithm that generated algorithms to (hopefully optimally) solve a certain graph problem. The evolutionary algorithm kept optimizing into bugs in my code, exploiting loopholes where I forgot checks and limits. It took multiple iterations and fixes until it stopped optimizing into bugs and coming up with impossibly good algorithms. AI does the same on steroids. It might indeed become nearly impossible to ascertain that AI didn't exploit the tooling to achieve the proof if the complexity involved is large.
The funny thing: In the end, the best algorithm the evolutionary algorithm found was exactly the same one I found by hand. But I couldn't construct a proof of optimality. I wonder if someone has come up with it in the meantime.
k749gtnc9l3w | 12 days ago
… and the fact that finding another bug in Lean might be easier than the problem, and the fact that LLMs are clearly overtrained to exploit bugs…
On the other hand, maybe if the proof is translatable into enough automatic checkers, it could be accepted.
This is the really important part: the tradition is to count proofs because this is a way to keep score, but the real question is whether a proof moves understanding forward or consists purely of pointless slog. Humans also do proofs out of slog, but generally humans figure out things in the process and smplify. LLMs don't get tired in the same way as humans, so they might succeed with slog that explains nothing but technically speaking proves the original statement as written.
Zero-knowledge proofs don't need to be cryptographically sound to be useless.
gignico | 12 days ago
Of course, maybe I was not clear in my statement. The point is not that I want to figure it myself. The point is that I enjoy reading a proof discovered by a human because it was discovered by a human. It’s the wonder for the capability of the human mind that inspires. Reading a machine generated proof would be not entertaining for me. Of course knowing the result may be useful. But not entertaining or inspiring like good math can be. But I suppose that’s just a matter of personal taste.
dutc | 12 days ago
There was a fantastic post by David Bessis previous shared here that seems of revelance.
Quoted: