Paper questions whether OpenAI's Lean proof matches the Navier-Stokes problem
Researchers argue that AI autoformalisation may have altered the original conjecture during translation from natural language to formal code.
What to know
- OpenAI's Lean 4 proof of Navier-Stokes blow-up compiles mechanically, but a new paper questions whether the AI's translation preserved the original problem statement.
- The central dispute: Does a formally valid Lean proof count as solving the conjecture if it may not match what mathematicians originally intended to prove?
- Commenters split between those who see mechanical correctness as sufficient and those who demand correspondence between formal and natural language statements.
The dispute Whether the Lean proof's mechanical validity suffices to claim a solution, or whether it must be validated against the original Clay Institute problem statement to matter. · positions read across 21 posts and comments
Mechanical validity is sufficient; the Lean proof solves whatever conjecture it formalizes, regardless of natural language correspondence.
-
“As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved".”
fasterik · Hacker News ↗
The Lean proof is only valid if it formally captures the original Clay Institute problem statement; autoformalisation may have changed the conjecture.
-
“If the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely…”
infogulch · Hacker News ↗
AI-generated proofs should be called claims and subjected to peer review before being treated as solved, to prevent circumventing the scientific process.
-
“I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them. The idea that an AI…”
j2kun · Hacker News ↗
Autoformalisation raises a fundamental theory-of-meaning crisis: formal proof correctness may not guarantee that the system proved what mathematicians intended.
-
“Will we ever run into a theory of meaning crisis? Assuming two failure modes: The lean kernel could always have a bug. The formalized statement may not correspond to what _mathematicians_ "actually wanted"”
sigbottle · Hacker News ↗
OpenAI Developer of contested Navier-Stokes proofAlexander Bastounis, Fabian Circelli, Anders C. Hansen arXiv researchers
The record 3 articles and posts · last 30 days
What people are saying 19 voices from 1 site · best of 21 · verbatim
- Oct 8
-
We talk about the AI proof while people are not focusing on the fact that AI had much more access to knowledge for three reasons.The first is that it filtered out rubbish. Yes, there is so much rubbish papers out there while good ones are lost in noise. The second is that it ingested data from countless journals. The average researcher does not…
- Oct 7
-
Navier-Stokes is an equation, not a theorem, so there is no such thing as "a proof of Navier-Stokes". The equation is a partial-differential-equation model of viscous fluid flow. Its correctness has never been in doubt: we know it cannot possibly be an exact description of real fluid flow, that it's a pretty good approximate description, and that…
-
Quote from paper worth being aware of:"Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."
-
This paper is a large amount of nothing. First, natural language is not as precise as lean, so you have multiple ways to translate a NL argument to Lean. As shown in Fig 1, the LLM did a decent job at translating the argument about roots in a succint way.Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean…
-
This is a bit delicious if I understand it correctly.They managed to find an excuse not to bother checking. They're saying that they refuse to verify the English paper because the lean had to be slightly changed to compile so there isn't a perfect 1:1 between the English paper and the compiled code.They're also saying that this ipso facto means…
-
The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the…
-
Will we ever run into a theory of meaning crisis?_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…
-
Given the high-level description of the examples, I think it's less of a "mis-translation" as it is the LLM tweaking the proof as it formalized it. Going between m+4 and m+5 is a pretty different thing than the sort of ambiguities that generally arise in parsing natural-language mathematical statements.
-
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
-
No, they're not claiming that.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…
-
Hm, looking through here, I don't see where they state what it is that OpenAI actually proved instead of Navier-Stokes blowup with forcing. I see where they do this for some other particular statements used along the way, but not for the headline result.
-
I read them as making a much weaker claim than this: not that the Lean proof isn't valid, just that it is not actually a formalization of the natural-language proof in the PDF they provided alongside it. I haven't heard any PDE people claim that the Lean proof is invalid, and I have heard things from a lot of them that imply that they think it is…
-
If I understand the abstract correctly (big caveat), they aren't saying they didn't prove it. They're saying they gave two proofs, one in natural language and one in Lean, that are not equivalent to each other. I assume the main significance is that the Lean proof is not a formal verification of the natural language one and the natural language…
-
Aside from the usual squabbling about AI, it seems the bombshell claim is this:"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…
-
As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved". The natural language proof is a "nice to have".
-
>The idea that an AI company is beyond peer review is harmful.i havent seen this sentiment expressed anywhere, have you?isn't this comment chain on a submission about openai's claims being reviewed?
-
I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them.The idea that an AI company is beyond peer review is harmful.
-
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?
-
I recently spent 3 weeks with claude formalizing a CS paper about a borrow checker in lean, for a personal project.The formalization went through, but there were _several_ mistakes in the original paper that it uncovered, from type setting errors to (many) formulas that quantified over all resources as printed, but actually applied to only arising…