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 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.

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, 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.

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?

For a refreshment of what is Navier-Stokes in a few words: https://p.migdal.pl/equations-explained-colorfully/#navier-s...

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 proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.

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.

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 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.)

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.

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 get the feeling a lot of people propose that we can write a verifier for every proof in lean.

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

It was a piston in a non-compressible fluid so to speak (ie. storm in a glass of water)

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 resources in the calculus..

So the formalization did give me a formally verified borrow checker that I could use to build a programming language on top of, but it was _not_ exactly the borrow calculus that was printed in the paper.

I expect this is the most common experience when mechanizing a printed paper. There are a lot of skipped steps and handwaving.

ok

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.

So my guess is that they have the AI system attempt to prove the theorem in natural language, then try to generate a Lean proof for it, and in that process they end up with a slightly different solution as the autoformalizer is essentially rewriting the NL proof to make it formalizable? Do we just need a "reverse pass" to re-align the NL proof with the Lean code?

Also, it doesn't seem that they are questioning the truthfulness of either proof, just that they are different?

Two leading experts on Navier Stokes still do not know whether their methods were used:

https://terrytao.wordpress.com/2026/10/04/on-classical-solut...

Humans will have to wade through mountains of slop to decipher the argument. Alternatively, they could just ignore it like Mochizuki's ABC proof prior to the Scholze/Stix refutation.

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

> In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation

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. So a model can translate a statement into a formal system and prove it, and the proof can check out, while the statement it proved isn't quite the one the mathematician meant. I read this article as a caution that some of the LLM proofs announced so far may not hold up once a human checks what was actually proved. Is that a fair reading?

Edit out vulgarity

This shouldn’t be a surprising result. We’ve known almost since LLMs became a thing that they can “prefer” modifying the terms or context of a problem when they can’t solve it directly (what one might call “cheating” if there were any volition involved). Often that happens in a way that isn’t immediately obvious to the user.

Before it was dropping databases or deleting repositories. Now it’s subtly changing the meaning of math problems to get a correct but irrelevant answer.