Overview
A team of mathematicians at the University of Cambridge has identified a critical mismatch between the two versions of OpenAI’s proof of the Navier-Stokes problem, published in September 2026. OpenAI released both a natural-language proof and a Lean 4 formalisation, explicitly claiming the latter was a direct encoding of the former. Researchers Anders Hansen and Fabian Circelli argue the two proofs do not correspond, meaning the computer-verified result may not confirm the human-readable argument.
The finding does not necessarily invalidate either proof — both could independently be correct — but it exposes a significant gap in how AI-generated mathematical outputs are being presented and trusted.
Technical Analysis
The failure mode is rooted in the auto-formalisation process. When an LLM translates natural-language mathematics into Lean 4, it must produce code that compiles — i.e., is internally consistent and passes the proof checker. If a direct translation of a proof step does not compile, the model seeks an alternative formulation that will. This alternative may be logically distinct from the original intent.
This is a form of semantic drift under syntactic constraint: the model optimises for a passing compiler output rather than for faithfulness to the source argument. The result is a Lean proof that is self-consistent and verifiable on its own terms, but which proves a subtly different — or more restricted — statement than the one articulated in natural language.
OpenAI’s GitHub repository states the Lean files contain “formalizations of the results presented in” the accompanying paper, an assertion the Cambridge team disputes.
Framework Mapping
- AML.T0031 – Erode AI Model Integrity: The auto-formalisation process introduces silent semantic errors that undermine the integrity of outputs presented as verified.
- AML.T0067 – LLM Trusted Output Components Manipulation: The Lean proof is positioned as a trust anchor (mechanically verified), yet its fidelity to the source is not guaranteed.
- LLM02 – Insecure Output Handling: The formalised output is consumed downstream as authoritative without adequate validation of its correspondence to the original proof.
- LLM09 – Overreliance: The broader issue is institutional overreliance on formal verification as a replacement for human peer review, without accounting for translation fidelity.
Impact Assessment
The immediate impact is reputational and epistemic rather than exploitative. However, the precedent is significant: if AI auto-formalisation is accepted as a peer-review substitute in mathematics, errors of this kind could propagate undetected into scientific literature. In higher-stakes applied domains — formal verification of software, cryptographic protocols, or safety-critical systems — this same failure mode could have operational consequences. The burden, as Hansen notes, falls back on human mathematicians to read and reconcile both proof forms.
Mitigation & Recommendations
- Do not conflate compilation success with semantic correctness — a passing Lean proof does not confirm it encodes the intended theorem.
- Mandate human diff review between natural-language and formalised versions before any claim of equivalence is published.
- Treat auto-formalisation as a tool, not a verifier — LLM-generated formal proofs should be subject to the same scrutiny as any other LLM output.
- Develop formalisation audit tooling that flags divergence between source claims and formalised statements at the definition level.