Paper: verified Lean proof of OpenAI's Navier-Stokes claim does not match the natural language proof

For a quick refresher on what Navier-Stokes actually is, this colored explainer is worth a look.

Hmm, I don't think that actually explains the idea of a momentum density transport equation well at all.

This is what I've been wondering about with LLM proofs. Math is logical, but mathematical writing is still natural language: symbols get overloaded, conventions go unstated, and a lot rides on context. A model can translate a statement into a formal system and prove it, the proof checks out, and the statement it proved isn't quite the one the mathematician meant.

Natural language is ambiguous, but the Lean formalization is well defined and unambiguous. The formal language isn't the real problem here. The ambiguity is on the other side, plus how hard it is to do a useful and accurate translation.

I spent 3 weeks with Claude formalizing a CS paper about a borrow checker in Lean for a personal project. The formalization went through, but it uncovered several mistakes in the original paper, from typesetting errors to formulas that quantified over all resources as printed when they only applied to arising resources. I got a formally verified borrow checker, just not exactly the calculus that was printed.

That's the common experience replicating a published paper by hand, you find 'obvious' steps that are anything but. The scary part is when AI generates unreadable formal proofs and then fabricates the natural language version of the steps, since that's the part people actually read.

As a second rate scientist, nothing makes me happier than finding a hot paper in my field, converting it to code, and showing the authors made systematic errors that make it more likely false than true. Attention goes to the hot, wrong papers.

I enjoy running into those details when implementing papers, it usually leads to better understanding and more rigor. It's also a lot of work, and we should be careful about relinquishing that sorting to AI.

If I'm reading this right, they're questioning the equivalence between the natural language proof and the Lean proof, not the correctness of the Lean proof?

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?

Right, there's no real pressure on the AI to get the natural language version of the proof correct, and no way to judge it automatically.

It doesn't look like they found an error in the natural language proof either, just that the two are different. Humans do this too: write a spec, implement it, the code doesn't work, fix the code and forget to fix the spec.

This shouldn't be surprising. LLMs have always preferred modifying the terms or context of a problem when they can't solve it directly, usually in a way that isn't obvious to the user. Before it was dropping databases or deleting repos, now it's subtly changing the meaning of a math problem to get a correct but irrelevant answer.

I've never used AI to translate between natural language and Lean, but I have gone from English to Golang, Python, TypeScript and SQL, and its interpretations can be creative.

At the very least, coverage of AI-generated proofs should describe them as claims to solve problems until the community has had time to review them. The idea that an AI company is beyond peer review is harmful.

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 enough to consider the problem solved. The natural language proof is a nice to have.

My guess is they have the AI prove the theorem in natural language, then autoformalize it, and the autoformalizer ends up rewriting the NL proof into something formalizable, giving a slightly different solution. Do we need a reverse pass to re-align the NL proof with the Lean code?

Generating the Lean proof first and adding an explanatory pass after is viable too. And yes, they are questioning whether the natural language description of the proof is unfaithful to the formal proof, simply wrong, or both.

Not a mathematician here. Why not just always use Lean? Why use natural language at all?

Same reason humans write code instead of machine code: so other humans can understand what we write, learn from it, and modify it. People need to understand what is being proven.