Comment by buzzy_hacker
7 hours ago
If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof?
7 hours ago
If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof?
If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
From the paper: "A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
The material is interesting, but unless the statement that is proved in lean is not blowup for Navier-Stokes, then it's still proven.
What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof.
A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult).
So the most fundamental question is: does the Lean theorem faithfully state the right theorem?
That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it.
For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.
Not quite — the formal statement of the problem in Lean may be correct, and therefore the Lean proof gives quite a lot of confidence that the statement is true. It's just that the proof given in natural language doesn't necessarily match up with the Lean proof, so the natural language proof might be unsound even though the statement it's proving is true.
I was having trouble wrapping my head around it but this cleared it up.
> If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.
> The natural language proof was derived from the lean code, badly.
Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
[1]: https://openai.com/index/navier-stokes-solution/
4 replies →
That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.
If your code compiles, are you sure it's bug free?
I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.
They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).
1 reply →
Not a mathematician, but "pretty sure" might not be good enough to resolve this question.
3 replies →
syntax vs semantics
It doesn't look like they've found an error in the NL proof either, just that they are different?
Indeed. The natural language proof is incorrect but the Lean proof is correct.
Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.
How do you know the natural language proof is incorrect?
Yes — because there are many non-equivalent statements that are easier to prove.
So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.
Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically.
Yes however, whether a natural language proof and a formal proof "correspond" is subjective.