In Brief
OpenAI mistranslated mathematics into code for its Navier–Stokes proof
Why this matters now: OpenAI’s high-profile Navier–Stokes claim is under scrutiny because an automated translation step between the published human-readable proof and the machine-checked Lean file appears to have introduced mismatches, raising questions about trust in AI-produced proofs.
OpenAI published what it presented as a proof of a Millennium Problem and shipped a Lean formalisation as a validation step. A new critique covered by New Scientist argues that the natural-language writeup and the Lean certificate don’t line up — not necessarily because the mathematics is wrong, but because the automated "autoformalisation" pipeline produced subtle, plausibly incorrect translations. As University of Cambridge’s Anders Hansen put it, “What has to be done with all of these large language model-generated proofs is that they will have to be read by humans, and this creates an enormous extra burden on mathematicians.”
The immediate fallout on community channels focused on two linked worries: autoformalisation is brittle and can produce plausible but mismatched artifacts, and labs chasing prestige may release machine-generated results without enough independent vetting or provenance. The consensus in commentary: Lean certificates are powerful, but they are not a substitute for careful human checking of the natural-language argument and the formal file.
Deep Dive
OpenAI mistranslated mathematics into code for its Navier–Stokes proof
Why this matters now: OpenAI’s publication and associated Lean formalisation are shaping expectations about AI-driven mathematics; failures in the translation pipeline could mislead the community and shift verification work from automated checks back onto overburdened human experts.
The scene: OpenAI released a paper claiming progress on the Navier–Stokes problem and included a Lean formalisation — a machine-checked artifact that purportedly backs the argument. Formal proof assistants like Lean are increasingly treated as gold-standard validators because a Lean proof, in principle, eliminates hand-checking errors. The critique reported in New Scientist finds that the human-readable proof and the Lean file diverge in meaningful ways after an automated translation step. That divergence is not just an academic nitpick: a mismatch can mean that the certificate is proving a different lemma than the one the prose claims, or that small syntactic shifts change the underlying mathematical claim.
Autoformalisation — the pipeline that turns natural-language math into a formal proof script — is seductive because it promises to scale formal verification. But the critique shows why it’s fragile. Autoformalisation systems must resolve ambiguous natural-language expressions, choose definitions and lemmas from large libraries, and stitch together proof steps that a human author might gloss. Any of those choices can introduce a semantic shift. In this case, the outcome was a Lean artifact that looked valid but did not faithfully reflect the natural-language argument. As the community reaction put it, a Lean certificate “does not guarantee correct natural language proofs.”
Why that gap matters practically: mathematicians read and trust prose explanations; they expect formal files to be faithful encodings, not edited or translated artifacts that stand alone. If labs treat a Lean file as a proof by proxy and stop there, readers may be misled. Conversely, if every autoformalised proof requires exhaustive human reconciliation, the efficiency gains from automation shrink. Anders Hansen’s point — quoted in the New Scientist piece — captures this tension well:
“What has to be done with all of these large language model-generated proofs is that they will have to be read by humans, and this creates an enormous extra burden on mathematicians.”
So what should the community and labs do? First, treat autoformalisation artifacts as companion outputs, not final adjudications. That means publishing precise provenance: which parts were machine-generated, which were human-edited, and what heuristics the translator used. Second, invest in independent replication: invite external proof engineers to re-encode or re-check the core lemmas in different proof assistants or via different autoformalisation runs. Third, tighten the tooling around ambiguity resolution — for example, require explicit specification of definitions where multiple conventions exist (function spaces, norms, boundary conditions). Those steps won’t eliminate errors, but they shift the workflow from "machine says so" to "machine helps, humans confirm."
There’s also a broader incentive problem. Big labs may be tempted to release headline-grabbing claims with machine-checked artifacts to demonstrate capability. That can accelerate research but also risks eroding trust if the artifacts are later found to be mismatched or irreproducible. The healthy middle ground is transparent collaboration: open the autoformalisation pipeline, include test cases, and fund independent verification teams. Proof assistants and Lean remain powerful tools — the lesson is that a certificate is a necessary condition for reliability, not a sufficient one.
“Navier–Stokes lost in translation” has become shorthand in some threads for the broader fragility of converting human mathematics into machine-checkable form.
Bold takeaway: A Lean certificate boosts confidence but does not eliminate the need for human scrutiny of the natural-language argument — particularly when the certificate is the product of automated translation.
Closing Thought
Autoformalisation is one of the most consequential AI-to-science ideas out there: if it works, it scales rigorous verification; if it fails silently, it risks amplifying errors under a veneer of machine authority. OpenAI’s Navier–Stokes episode is an early, public stress test. The sensible path forward is not to reject formal methods, but to demand clearer provenance, more human-in-the-loop checkpoints, and a culture that prizes independent verification over single artifacts that look finished.