I think this paper also misses that if an LLM can exploit a bug in Lean, it will.
They're just optimizers that are driving towards maximizing a goal. If they're plugging along and they get incorrect output from Lean, they'll happily use that as a tool to solve the proof.
So if you have a million-line-long Lean proof of something, you're faced with not ever being quite certain that there isn't some "...and then a miracle occurs..." exploit of Lean somewhere in the middle of it.
The one buggy AI Lean proof I’m aware of was a case where someone found a soundness bug in Lean (with or without AI, I’m not sure) then announced the Collatz conjecture to be proved using that bug they found. It was understood to be buggy within a day.
Are there other cases I’m not aware of where an announced proof was found to be based on exploiting a Lean bug?
Obviously unsoundness in the Lean kernel is an issue (which we can't rule out), but I agree with my sibling commenter that this seems quite unlikely to be missed assuming there is a reasonable effort to review the proof. I'm not a Lean expert, but I do formal methods (and know Lean experts myself) and my intuition is that soundness exploits will look something like deriving false. I'm not saying it's trivial to detect something like this (mumble mumble undecidability), but I do think it will smell.
An example of what I mean is if you have a function in Haskell foo :: Enormous -> () whose input is some really complicated type. And you see something like
bar = foo x
-- this is an infinite loop, so it can have any type
where x = let y = y in y
Note also that the paper makes no claims about the invalidity of the Lean proof itself, but only of the mismatch between NL and Lean. Frankly it would be a feat almost as impressive as the N-S proof (which I understand to be enormous) if the Lean translation was 100% faithful to the NL (due to size).
TL;DR: IMO this paper and the possibility of unsoundness should not be taken as evidence that "LLMs can't do proofs." Especially for gargantuan proof artifacts, the only way I would want to interact with a sizable LLM proof is via a theorem prover precisely because NL proofs have no way to rigorously and systematically check them.
Let it be known that I was saying two years ago that LLMs should be amazing at doing proofs precisely because they're machine-checkable (they sucked at proofs during this time). Judging from what the mathematicians are saying I'm not exactly thrilled to be proven right.
Disclaimer: I don't write Lean. I would say that at least a review of any instances of falsity plus a shallow review of the main components of the theorem. But I don't know what best constitutes a human audit of machine-checked code.
Believe me, I'd love to be proven wrong, but I gotta trust the mathematicians and experts here. The proof is out there AFAIK (I mean if they haven't released it then maybe yeah I would say we should be skeptical). If enough time passes we can assume it to be proven (or useless/uninteresting enough to the broader community for its veracity to not matter, in which case we should dismiss the proof for the PR stunt it is, not for the possibility of kernel bugs).
I think this paper is worth reading, and does highlight a valuable caution about the relationship between natural language proofs and Lean formalizations, especially in the case that they were generated by agents. There really is significant room for slippage.
That said, it's important not to draw too strong a conclusion. The most likely scenario is that there is slippage between the Lean proofs and the natural language proofs. This does not by itself imply that the natural language proof is fundamentally wrong, or that the theorems have not been proven.
As long as the Lean statement properly captures the proposition in question, the Lean proof is almost certainly accurate. And if the Lean proof doesn't capture the proposition, you'll hear about if for the major results ("OpenAI didn't really solve Navier-Stokes" would be enormous news).
In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy/arithmetical hierarchy (the SCI =∞)
This is very fascinating. I hope to understand this better tomorrow.
dualvariable | a day ago
I think this paper also misses that if an LLM can exploit a bug in Lean, it will.
They're just optimizers that are driving towards maximizing a goal. If they're plugging along and they get incorrect output from Lean, they'll happily use that as a tool to solve the proof.
So if you have a million-line-long Lean proof of something, you're faced with not ever being quite certain that there isn't some "...and then a miracle occurs..." exploit of Lean somewhere in the middle of it.
hyperpape | a day ago
The one buggy AI Lean proof I’m aware of was a case where someone found a soundness bug in Lean (with or without AI, I’m not sure) then announced the Collatz conjecture to be proved using that bug they found. It was understood to be buggy within a day.
Are there other cases I’m not aware of where an announced proof was found to be based on exploiting a Lean bug?
cole-k | a day ago
Obviously unsoundness in the Lean kernel is an issue (which we can't rule out), but I agree with my sibling commenter that this seems quite unlikely to be missed assuming there is a reasonable effort to review the proof. I'm not a Lean expert, but I do formal methods (and know Lean experts myself) and my intuition is that soundness exploits will look something like deriving
false. I'm not saying it's trivial to detect something like this (mumble mumble undecidability), but I do think it will smell.An example of what I mean is if you have a function in Haskell
foo :: Enormous -> ()whose input is some really complicated type. And you see something likeNote also that the paper makes no claims about the invalidity of the Lean proof itself, but only of the mismatch between NL and Lean. Frankly it would be a feat almost as impressive as the N-S proof (which I understand to be enormous) if the Lean translation was 100% faithful to the NL (due to size).
TL;DR: IMO this paper and the possibility of unsoundness should not be taken as evidence that "LLMs can't do proofs." Especially for gargantuan proof artifacts, the only way I would want to interact with a sizable LLM proof is via a theorem prover precisely because NL proofs have no way to rigorously and systematically check them.
Let it be known that I was saying two years ago that LLMs should be amazing at doing proofs precisely because they're machine-checkable (they sucked at proofs during this time). Judging from what the mathematicians are saying I'm not exactly thrilled to be proven right.
landon | 21 hours ago
What is a "reasonable effort" to review a million lines of lean?
cole-k | 19 hours ago
Disclaimer: I don't write Lean. I would say that at least a review of any instances of falsity plus a shallow review of the main components of the theorem. But I don't know what best constitutes a human audit of machine-checked code.
Believe me, I'd love to be proven wrong, but I gotta trust the mathematicians and experts here. The proof is out there AFAIK (I mean if they haven't released it then maybe yeah I would say we should be skeptical). If enough time passes we can assume it to be proven (or useless/uninteresting enough to the broader community for its veracity to not matter, in which case we should dismiss the proof for the PR stunt it is, not for the possibility of kernel bugs).
Garbi | a day ago
I've been wondering if that proof used the Kobayashi Maru method. Glad to see others seriously considering that possibility.
hyperpape | 22 hours ago
I'll share a comment I made on HN: https://news.ycombinator.com/item?id=49995154.
I think this paper is worth reading, and does highlight a valuable caution about the relationship between natural language proofs and Lean formalizations, especially in the case that they were generated by agents. There really is significant room for slippage.
That said, it's important not to draw too strong a conclusion. The most likely scenario is that there is slippage between the Lean proofs and the natural language proofs. This does not by itself imply that the natural language proof is fundamentally wrong, or that the theorems have not been proven.
As long as the Lean statement properly captures the proposition in question, the Lean proof is almost certainly accurate. And if the Lean proof doesn't capture the proposition, you'll hear about if for the major results ("OpenAI didn't really solve Navier-Stokes" would be enormous news).
srcreigh | 18 hours ago
This is very fascinating. I hope to understand this better tomorrow.