Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean ones. My understanding is that the translator LLM got lazy and wrote the minimal amount of code that satisfied the theorem without the extra stronger claims.
It is common in mathematical papers to say "And by the way, this actually proves [stronger claim]", but this is something an AI with a precise goal of performing a translation would never do, as it's goal is to translate the proof, not to quality mathematics.
"In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
https://github.com/google-deepmind/formal-conjectures/blob/8...
;)
Did you mean “not…correctly”?
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."
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?
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.
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.
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.
That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
If your code compiles, are you sure it's bug free?
Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true.
Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim.
Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type.
The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)?
The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect.
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.
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.
I don’t think that actually explains the idea of a momentum density transport equation well at all.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.
[1]:https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
[2]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
_Assuming_ two failure modes:
- The lean kernel could always have a bug. - The formalized statement may not correspond to what _mathematicians_ "actually wanted"
It seems natural to make the argument of, "Well, even if you make the argument that the proof can have mistakes, it's surely easier to check the problem statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments correct" according to the _second_ criteria - maybe in the natural proof it invents an object subtly different from the formal one, but it all checks out. If you guarantee that the _original_ statement corresponds, then the only possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have good theories for? How do you quantify how much descriptive power you need to express a question? Often times in math, the hard part is getting the definition right - but what if the definition itself starts to become so complex and unverifiable that no one can correspond that to anything? Well, it seems like many interesting long-standing math problems have "relatively" simple problem statements, in such a way that you could formalize it to lean easily, but not sure if there's really a silver bullet w/ lean or if it's going to be turtles all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its a generalized theory of semantics.)
Can someone tell me in simple terms why this doesn't conflict with the incompleteness theorems?
edit: thanks for the responses, i feel slightly less dumb now
We know as a consequence of Goedel theorems (at least I believe so), that there is no algorithm that would take a statement and output a proof if it is provable or a counterexample if it is not. However, AI provers never give anything for sure, so I think there is no contradiction here.