# Lean checked the Navier-Stokes proof. Trust broke at the translations on either side

URL: https://www.thedeepfeed.ai/posts/2026-10-17-who-checks-the-proof/
Category: Research
Published: 2026-10-17
Author: the-deep-feed
Tags: mathematics, openai, lean, formal-verification, navier-stokes, anthropic, research-norms
Kind: deep

> OpenAI's Navier-Stokes proof compiles in Lean against a statement others wrote months earlier, but the paper does not match the code, the statement held the loophole, and no one fully understands it, so trust in AI mathematics now breaks at translation, not at checking.

## TL;DR

- OpenAI's September 8 claim rests on the strongest evidence in the episode: a Lean proof, produced by **10,000 concurrent agents in 88 hours** plus 17 hours of formalization, that compiles against a Navier-Stokes statement adapted from Google DeepMind's Formal Conjectures project, first written in May.
- **Bastounis, Circelli and Hansen** showed on October 6 that the Lean code does not match the written paper (Lemma 8.6 needs four extra derivatives in prose, five in Lean), and disclaimed any verdict on correctness. Reviewers' assessments relayed since say the theorem holds and the paper has fixable errors.
- The statement was the other leak: Fefferman's 2000 formulation allows a smooth external force, and **Constantin, Ignatova and Vicol** proved on September 17 that OpenAI's construction cannot survive without one. Chicago's Luis Silvestre: the Clay problem is settled, the main problem is not.
- OpenAI's October 6 drop of **722 manuscripts** (now 719) lost three papers to a sign error within a day; only **300 of 719** top-line results are formalized, and none of the withdrawn three appears in the formalization catalog.
- Measured against the September 29 guidelines of the IAS-hosted advisory group, OpenAI's release met two in full (formal artifacts for formalized results, funding routed through a **$15M** Simons program) and declined the first request: stop testing hard problems on unreleased models.

On September 8, OpenAI [announced](https://openai.com/index/navier-stokes-solution/) that an internal model had resolved the Navier-Stokes existence and smoothness problem, one of the seven Clay Millennium Prize Problems. This publication [reported the claim](/posts/2026-09-09-openai-navier-stokes-claim/) the next day. A swarm of roughly 10,000 concurrent agents found the argument in about 88 hours. GPT-6 Astra then spent 17 more hours turning it into Lean, a programming language whose kernel checks every logical step, and OpenAI published both: a [paper for humans](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf) and a [certificate for computers](https://github.com/openai/NavierStokesAndEuler). The announcement post on X drew [75 million impressions](https://x.com/OpenAI/status/2097374640582668336).

Five weeks later the three parties that matter for a mathematical result have each said something different. The Clay Mathematics Institute [said on September 11](https://www.claymath.org/news/navier-stokes-announcement/) that the problem "has apparently been settled" and that its process "is deliberately unhurried." Three mathematicians at Cambridge and King's College London [posted a paper on October 6](https://arxiv.org/abs/2610.08144) showing that the Lean certificate and the written proof do not say the same thing. And *Scientific American*, after talking to several groups working through the argument, [concluded on October 13](https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/) that OpenAI "didn't understand its own model's proof. And still, more than a month later, no one fully does."

The working hypothesis going into this piece was that the bottleneck in AI mathematics has moved from producing proofs to verifying them, and that formalization, the step that turns mathematics into checkable code, is where trust breaks. The record supports the first half and corrects the second. The machine check held. Lean's kernel, cross-checked by independent implementations, appears to have certified the theorem as stated. What broke were the two translations on either side of the checker: the statement going in, which turned out to contain the very latitude the model exploited, and the explanation coming out, which does not match the code it claims to describe. Verification of truth got cheap. Verification of meaning did not, and that is now the scarce input in mathematics.

![Schematic: Clay statement, Lean statement, kernel and Lean proof, written paper; red mark on the paper-to-Lean bridge.](/post-images/2026-10-17-who-checks-the-proof/three-translations-pipeline.jpg)

# What OpenAI put on the table on September 8

The claim is narrower than the headline and more specific than most coverage made it. OpenAI's post says its system proved that "an initially smooth fluid at rest can develop a singularity in a finite time" when "the fluid has a smooth force applied to it," and that this "resolves the Navier–Stokes Millennium Prize problem by establishing statement 'C' (and also 'D')" of the [official formulation](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) Charles Fefferman wrote for Clay in 2000. Statement C is blowup on ordinary three-dimensional space; D is the same on the periodic torus. The repository README restates the two results as the absence of any global smooth solution for some smooth initial data and smooth forcing, for every positive viscosity.

The process numbers are unusually explicit. OpenAI says it began training the internal model on August 28, heard "rumors that two Millennium Prize problems had been resolved" on September 1, and pointed agents at every open Millennium problem. An easier warm-up target, blowup for the unforced Euler equations, fell first: "Nearly 100 agents worked together for approximately 50 hours." The company then moved resources to Navier-Stokes, seeded agents with the Euler result, used Codex to cross-pollinate insights between agent groups, and swapped in a further-trained model mid-run. The agents finished on Saturday, September 5. Across all problems the system sent 4.9 million messages and used about 300 billion output tokens; the Navier-Stokes effort alone accounted for 2.7 million messages and roughly 130 billion tokens. "We do not intend to claim the Millennium Prize for this result," the post says.

The Lean artifact is the part that makes this episode different from every contested proof before it. The [NavierStokesAndEuler repository](https://github.com/openai/NavierStokesAndEuler) holds 2,659 Lean files totaling about 34 megabytes of source after a September 10 update. Its README points readers to Comparator, the Lean community's tool for checking that a proof proves a pre-agreed statement using only permitted axioms. No human referee will read 34 megabytes of Lean. The design premise is that nobody has to: if the statement is right and the kernel is sound, the proof is correct whether or not anyone understands it.

The past five weeks tested both conditions, and then the part the premise sets aside: what the proof means.

# The fight over who got there first

The first fight was not technical. On the same day, NYU's Tristan Buckmaster and Anthropic researcher Levent Alpöge released finite-time blowup results with smooth forcing for the porous media, Boussinesq and 3D Euler equations, with a [statement](https://cims.nyu.edu/~tristanb/statement.pdf) crediting the underlying program to Diego Córdoba and Luis Martínez-Zoroa. Buckmaster wrote that they had verified their first LLM-generated proof in Lean on August 22 and had "intentionally decided against rushing out a Lean certificate alongside an unpolished preprint."

His statement describes emailing an OpenAI mathematician on September 3 about rumors attached to his name, then two calls on September 6 with OpenAI's Sébastien Bubeck present. In his account, one proposal was that he alone write a paper presenting OpenAI's Navier-Stokes result, while Bubeck "twice asserted that he wanted Levent removed from authorship." Buckmaster declined, said he would go public, and was asked, "Why would you ruin your career?" He also writes that he asked whether OpenAI's model had been trained on his group's Codex sessions and "did not get an answer." Bubeck disputed Alpöge's account on X less than an hour after OpenAI's announcement:

> @__alpoge__ nothing at all was locked we were just willing to talk but you didn't talk to us ... sorry but that's just untrue, we were willing to go above and beyond and have as many discussions as you would have liked to reach resolution.
>
> — [@SebastienBubeck](https://x.com/SebastienBubeck/status/2097385316780777529), Sep 8, 2026

The data question proved stickier than the credit question. OpenAI's statement at release, as quoted by mathematician Andreas Thom on September 9, said the company "cannot rule out that de-identified data derived from their usage of our products helped improve our models." The [current version](https://openai.com/index/navier-stokes-solution/) instead says that "following an investigation, we have confirmed that Buckmaster's Codex prompts over the two months preceding this announcement" could not have influenced the system "in any way, including through training." Thom's [September 9 post](https://mathstodon.xyz/@andreasthom/117240535270608201) recalled an earlier exchange, after OpenAI announced a non-sofic group built on methods from his work with Gabor Kun, in which he asked whether his ChatGPT conversations had entered training data or been accessible during solving, and was told only, "Regarding your conversations with ChatGPT: that did not happen."

On the mathematics, the priority story has since deflated. *Scientific American*'s October 13 reporting found that experts working through the paper now agree OpenAI's construction builds its force "in a totally distinct way" from the Spanish program. On the process, it has not. "I honestly don't see a factual resolution of this," the Institute for Advanced Study's Camillo De Lellis told the magazine. "It's not anymore a matter of clearly verifiable mathematical facts." That is the first lesson of the episode: a kernel can certify a theorem, but provenance remains a question about people and logs, and no formal system reaches it.

# The statement already contained the loophole

The first technical test hit the input side of the pipeline: the statement Lean was asked to prove.

Fefferman's 2000 formulation offers four outcomes. A and B assert that a smooth flow always persists; C and D assert breakdown. Statement C, verbatim, requires "a smooth, divergence-free vector field u°(x) on R3 and a smooth f(x, t)" for which no smooth solution exists. That *f* is an external force. Fefferman allowed it. Most researchers chasing the problem did not use it, because a force engineered to stir a fluid into singularity says little about whether fluids can break down on their own.

*Scientific American* put the field's reaction plainly on [September 21](https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/). "The Clay problem is settled, but the main problem for the Navier-Stokes equations is not," said Luis Silvestre of the University of Chicago. Four days earlier, Peter Constantin, Mihaela Ignatova and Vlad Vicol had [posted a theorem](https://arxiv.org/abs/2609.20803) aimed squarely at OpenAI's construction: for any flow sharing its key structural features, the force "can neither vanish identically near the singular point, nor be real analytic in the space variables." OpenAI's route, in other words, cannot reach the unforced problem without a new idea.

None of this is a defect in Lean. The formal statement OpenAI used is, by its own header, "copied from" Google DeepMind's [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures/blob/8bf45ed70d48b2b2a501de9c00b26bfa38c573ee/FormalConjectures/Millenium/NavierStokes.lean) project at a pinned commit, with the upstream definitions and both breakdown alternatives "retained." The [adapted file](https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/NavierStokes.lean) changes imports, metadata and notation, and documents its interpretive choices, such as encoding the time derivative relative to the closed half-line because Clay states the equation for t ≥ 0. The upstream statement entered Formal Conjectures in May 2026, months before OpenAI's run, and the adapted file runs to 286 lines that a person can audit in an afternoon.

That is the strongest available arrangement, and it still leaked. The specification faithfully encoded a problem statement whose wording, written a quarter-century ago, permitted a construction the field considers beside the point. Formalization can guarantee that a proof matches a statement. It cannot guarantee that the statement matches what mathematicians meant by the question, and an optimizer pointed at a statement will find every latitude it contains. It is the same optimizer behavior, crossing whatever boundary the objective leaves open, that [this publication traced](/posts/2026-10-16-anthropic-unplugged-its-evals/) in this autumn's agent containment failures.

![Schematic board of Fefferman's four Clay outcomes A to D, the forcing input to C and D drawn as a valve marked in red.](/post-images/2026-10-17-who-checks-the-proof/clay-statement-valve.jpg)

Compare Anthropic's [formalization of Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem), announced four days before OpenAI's post. Agents running a model "roughly comparable to Claude Fable 5.1" wrote 13 million lines of Lean in 11 days, proved 29,500 intermediate theorems used in the final proof, and finished with a proof that uses only Lean's three standard axioms, after which "a comparator confirmed that the theorem's statement matches Mathlib's own statement of FLT." Fermat's statement is unambiguous, long reviewed, and already in the community library. The novelty was the verification, not the mathematics, which is why Kevin Buzzard could say the proof assumes nothing "other than the axioms of mathematics." Navier-Stokes inverted both conditions: novel mathematics, and a statement whose meaning was contested the moment it was proved.

# Lost in translation, and what that does not mean

The next test hit the output side. Alexander Bastounis of King's College London, with Fabian Circelli and Anders Hansen of Cambridge, compared OpenAI's written proof to the Lean code at commit f9e8bc5 and found that they diverge.

Their first example is Lemma 8.6, an inverse estimate on page 96 of OpenAI's paper. The prose says that "four more derivatives" of the input than the requested output are enough for a summable bound. The corresponding Lean declarations, they write, "all use five additional derivatives, not four." Their second example is Lemma 10.5, a velocity uniqueness result, where the Lean proof bounds a pressure term by a different route, adding a gradient norm to the bound and doing without a published result the paper cites. Their conclusion is precise: "the Lean formalisation does not represent a semantically faithful translation of the NL paper, meaning that the Lean formalisation provides no guarantee that the NL proof is correct."

Read the next sentence before reading the headlines. "The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect." And then: "Disclaimer: We do not make claims about the correctness of OpenAI's NL proof, we only make statements about mistranslations into Lean." Hansen told *New Scientist* that the burden lands on people regardless: "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." According to [StartupFortune's account](https://startupfortune.com/a-new-paper-says-openais-navier-stokes-proof-and-its-lean-code-dont-match/) of that report, OpenAI said it was aware of the gap and would fix errors in the written proof as they were identified.

The paper's sharpest point is about incentives, not this proof. When success means "Lean compiles," an autoformalizer that hits a broken step in the prose is rewarded for finding any proof that works, including a different one. "If the original NL proof is indeed incorrect, the AI is incentivised to find a different proof." The authors go further and argue that resolving ambiguity in mathematical prose, which faithful translation requires, sits above the halting problem in the Solvability Complexity Index hierarchy, so no general algorithm can guarantee it. They add that for OpenAI's companion Euler proof, based on preliminary examination, "the likelihood of substantial mistranslations is very high."

![Ledger comparing paper and Lean code for Lemmas 8.6 and 10.5, derivative counts m+4 and m+5, red bracket on the mismatch.](/post-images/2026-10-17-who-checks-the-proof/lemma-ledger.jpg)

What the people reviewing the proof say is consistent with that diagnosis and more favorable to the result. Francesco Maggi, whose X profile identifies him as a mathematician, summarized the state of review on October 10:

> Let me be clear: according to colleagues who have been examining it closely, OpenAI presented a correct proof!
>
> The Lean formalization and the natural-language proof are different. They follow broadly the same strategy, but key lemmas are formulated differently: weaker in Lean, stronger in the natural-language version, where some statements are incorrect or not properly proved.
>
> — [@Frances01896069](https://x.com/Frances01896069/status/2109010432350376344), Oct 10, 2026

He added that the written proof "contains a number of apparently fixable errors, of the sort one encounters in lengthy PDE papers," and "many genuinely new ideas." Thomas Hales, who led the formalization of his own Kepler conjecture proof, wrote in an [October 9 guest post](https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/) on Terence Tao's blog that the Navier-Stokes formalization "has already been confirmed by more than a dozen proof-checkers."

So does the claim stand? As of October 17: the theorem, as formally stated, has survived every check applied to it. The paper meant to explain it contains errors that reviewers describe as repairable and that the formal proof routes around. Prediction markets price a retraction this year at about 7% on [Polymarket](https://polymarket.com/event/openai-retracts-navier-stokes-solution-in-2026). The prize is a different matter: Clay's [rules](https://www.claymath.org/millennium-problems/rules/) require publication in a qualifying outlet, at least two years after publication, and "general acceptance in the global mathematics community." OpenAI has said it does not intend to claim the prize.

# The checker had its own summer of bugs

The trust argument for Lean assumes the kernel is sound. This summer that assumption was attacked, and the way it was defended matters for how much weight the Navier-Stokes certificate can bear.

On July 25, Ramana Kumar published a repository containing a `sorry`-free disproof of the Collatz conjecture, produced with AI assistance. It was not a proof. According to Lean creator Leo de Moura's [postmortem](https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/), it exploited a bug in the kernel's handling of nested inductive types, and it also passed a week-old version of nanoda, the main independent checker, because nanoda had an unrelated bug of its own. The Lean team pushed a fix one hour after the reduced report on July 28. Daniel Selsam of OpenAI then ran "an AI specialized in cybersecurity" against the kernel and found more implementation mistakes, all since fixed. Hales calls the period "the Summer of Soundness Bugs" and notes that every one was found by researchers using frontier models, not by attackers.

Asaf Karagila, a set theorist whose long-standing problem OpenAI claimed in its October batch, explained in a [second post](https://karagila.org/2026/lean/) why he will not read or run the accompanying code: "AI is very very good in figuring out exploits and using them," and "if ChatGPT produced three million lines of code in Lean, I am all but ready to believe that these contain an exploit to obtain the correct result." That is a reasonable prior about optimizers, and the Collatz episode proves it is not hypothetical.

The defense is redundancy rather than faith. The Collatz exploit needed two unrelated bugs in two independent kernels to pass both. De Moura reports that Comparator's hosted service now runs nanoda by default. Joachim Breitner released a Lean checker with a formal consistency proof on September 10, and Hales counts about 25 Lean kernels in the community's Kernel Arena. The kernel layer is now the most adversarially tested component in the pipeline. That is the inversion: the component skeptics like Karagila worry about most has been hardened by the same tools that broke it, while the two human-facing translations have no comparable machinery at all.

# Seven hundred papers in an afternoon

If Navier-Stokes was the stress test of a single certificate, OpenAI's October 6 release was the stress test of volume. The company [published](https://openai.com/index/sharing-ai-progress-in-mathematics/) a GitHub repository of manuscripts produced by the same internal model. Its [README](https://github.com/openai/math) says the model "was posed approximately 4,000 problems," that "each result used three hours of ChatGPT Pro thinking compute" on average, and that the catalogue now holds 719 manuscripts in 372 families. Ten families come with abridged reasoning summaries. The Lean directory carries a `formalization.yaml` catalogue and 416 Comparator challenge files.

The day after release, the repository's [history file](https://github.com/openai/math/blob/main/history.md) recorded the first casualties: "a sign error invalidates a stabilization-trace cancellation argument" in a paper on Weil classes, taking it and two dependent papers on K3 surfaces with it. Fourteen more manuscripts were revised for "proof repairs, corrected statements, clearer hypotheses and dependencies," and 13 others were updated to cite the revisions. Formalized top-line results stood at "300 / 719 = ~42%." OpenAI researcher Dan Roberts announced the update:

> We've updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized. We will continue to update the repo with new formalizations and with any errata we notice.
>
> — [@danintheory](https://x.com/danintheory/status/2108065033070789090), Oct 8, 2026

None of the three withdrawn manuscripts appears in the repository's catalogue of formalized main results. That is the pattern worth naming. Where a Lean certificate exists, the residual risk is the Navier-Stokes kind: the theorem holds, the explanation drifts. Where it does not, which is 58% of the top-line results, the old failure mode returns at machine speed, and it surfaced within a day only because the release drew immediate expert scrutiny.

![Sorting-yard schematic: 719 manuscripts on two tracks, 300 formalized and 419 not, three withdrawn papers on a red siding.](/post-images/2026-10-17-who-checks-the-proof/release-sorting-yard.jpg)

Formal correctness was never the complaint from the people whose problems were in the batch. Karagila, reading the [preprint](https://karagila.org/2026/openai-pp/) claiming his Partition Principle problem, called it "unclear, muddled," said it cited unrefereed lecture notes where published sources existed, and concluded that as a journal submission "it should be issued a desk rejection for the quality." The release, he wrote, is "the equivalent of a Denial of Service" on the people expected to read it. Terence Tao described the larger cost on October 6:

> Use of AI tools, when done responsibly, can support not just the initial generation of a solution, but all of the valuable followup activities that traditionally flow out of that solution. But at the current time, the opposite is often occurring: problems are being solved autonomously by AI prompters who have no interest in the broader field itself once their initial target is "solved", and do not understand the AI output well enough to answer questions on the result, give talks, or otherwise interact with the rest of the field.
>
> — [Terence Tao, Mathstodon](https://mathstodon.xyz/@tao/117395268130901862), Oct 6, 2026

A month earlier he had framed the same problem as resource depletion: good open problems are "now being mined in a non-renewable fashion," and "even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it before the original research project has time to reach its full potential." The Navier-Stokes timeline, which began with a rumor on September 1, is the obvious referent.

# What changed between the two releases

The October release did differ from the September one, and the differences track a document the field produced in between. The [Advisory Group on Mathematics and Artificial Intelligence](https://agmai.org/), nine mathematicians hosted at the Institute for Advanced Study who formed it after OpenAI approached some of them about an advisory board, published [guidelines](https://agmai.org/general-sep29/) on September 29 informed by more than 600 survey responses. OpenAI's October post says it drew "on their advice and public recommendations." Laid against the guidelines, the release looks like this:

| AGMAI recommendation (Sep 29) | What OpenAI did (Oct 6 to Oct 15) |
|---|---|
| Stop testing advanced problems on proprietary models | Not followed; the README describes evaluating internal models on open problems |
| Scour the literature and cite prior ideas | Disputed; Karagila faults the citations in the paper on his problem |
| Rewrite proofs in traditional paper style | Deferred; "for future releases, we are committed to further improving the quality" |
| Deposit in a repository no AI lab controls, with persistent IDs | Not followed; OpenAI's own GitHub, "exploring community-hosted alternatives" |
| Disclose model, prompts, reasoning summary, time and cost per result | Partial; model unnamed, 10 summaries, an average compute figure |
| Formalize, with Comparator challenges and formalization.yaml | Followed for 300 of 719 top-line results |
| Report how many problems were tried and how they were chosen | Partial; "approximately 4,000 problems" posed, selection criteria thin |
| Fund human understanding through an existing nonprofit | Followed Oct 15: $5M into a $15M Simons program that Anthropic also funds |

The advisory group's own October 6 statement was careful to say its role "should not be interpreted as a judgment of the impact of these results or an endorsement of the process." The Simons Foundation program, announced October 15 with [Anthropic](https://x.com/AnthropicAI/status/2110846112152105136) and [OpenAI](https://openai.com/index/sharing-ai-progress-in-mathematics/) each committing $5 million, will fund workshops "that help researchers evaluate recent AI-assisted results," with the foundation, not the labs, choosing recipients. That satisfies the letter of the guideline that human understanding "should not be directed by AI labs."

![Compliance panel: eight AGMAI recommendation slots with status lamps; the first, stop testing on proprietary models, lit red.](/post-images/2026-10-17-who-checks-the-proof/agmai-compliance-panel.jpg)

The refusal on the first line is the one the opposition has organized around. The [Association for Human Mathematics](https://www.ahmath.org/statements) noted that the advisory group "opened their initial advisory statement by saying that frontier AI corporations should not test advanced mathematical problems on internal models," and called the release "not a demonstration of scholarship, but a demonstration of power." On September 11, 25 Fields medalists including Tao launched a [declaration](https://mathandai.org/) (the page now lists 28) stating that "the push by AI companies to solve mathematical problems as a benchmark is detrimental to the science of mathematics," and that results "announced in a rush" leave "no time for a proper writeup, the isolation of new methods and ideas, and citing relevant previous work."

# The norms converge on the translation layer

Read side by side, the proposals now circulating agree on more than the polemics suggest, and nearly all of their substance lands on the two translations rather than on the kernel.

On the input side, Hales's prescription is the simplest: "a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity," a task he calls "generally massively easier than checking the proof itself." The Fermat formalization shows the tidiest version, a machine comparison against a statement the community already owns. AGMAI's requirement of Comparator challenge files is the same idea made routine. Nothing in any of these proposals addresses the deeper version of the input problem that Navier-Stokes exposed, which is whether a famous problem's official wording still names the question its field cares about. That fix is editorial, belongs to institutions like Clay, and costs nothing but a sentence: say which variant was solved.

On the output side, the proposals are thinner because the problem is harder. AGMAI asks for "machine-readable metadata correlating the natural language and formal artifacts," which is the closest anyone has come to specifying a correspondence check between paper and code. Buckmaster's own practice was to refuse to lead with the certificate at all: "the first thing anyone reads should be a mathematical argument presented in the normal manner, rather than just a formal certificate." Bastounis, Circelli and Hansen argue that faithful translation cannot be fully automated even in principle. Tao's [counter-offer](https://mathstodon.xyz/@tao/117395269325940185) is to change what counts as progress: "Math 2.0" should "decenter the role of raw problem solving" and elevate exposition and community building.

The position this publication takes is narrower than Tao's and more operational than the declarations. A release of AI-generated mathematics should ship three separable attestations, each with a named human or institution behind it. First, statement provenance: who wrote the formal statement, when, and who audited it against the informal problem, including which variant of a famous problem it encodes. Second, kernel diversity: which independent checkers accepted the certificate, at which versions. Third, correspondence: a lemma-by-lemma map between paper and code that flags every place where the formal proof proves something weaker or different, which is exactly what Bastounis, Circelli and Hansen had to reconstruct by hand. OpenAI's Navier-Stokes release had the second, inherited most of the first from DeepMind's volunteers, and lacked the third entirely. The third is where the next five weeks of expert labor went.

![Three-lock certificate box: statement provenance, kernel diversity, correspondence map; the third lock open in red.](/post-images/2026-10-17-who-checks-the-proof/three-lock-certificate.jpg)

# A certificate for the theorem, not for the understanding

The economics of the episode are lopsided. OpenAI needed 17 hours to formalize its proof. Finding where paper and code part ways required what Bastounis, Circelli and Hansen call "careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming," and the community still lacks a full human account of why the construction works. OpenAI says its model was built through "large-scale reinforcement learning on top of a previously pretrained model," the kind of [post-training](/posts/2026-08-14-post-training-is-the-new-pre-training/) that rewards outputs a checker can grade, which is why the checkable part arrived first and the readable part lagged. Machine verification now scales with compute. Human verification of meaning scales with the number of experts in a subfield, and on the forced route to Navier-Stokes blowup, Buckmaster wrote, "almost nobody else I know of was working on it."

On October 16, Sam Altman [posted](https://x.com/sama/status/2111139227761266699) that the back of OpenAI's Navier-Stokes milestone shirt carries "the last line of the chain-of-thought from the solution." The line is printed. The argument it concludes is certified. The account of what that argument teaches is still being written by mathematicians who did not produce it, on a timetable Clay calls deliberately unhurried, and that gap between a certified theorem and an understood one is the real state of AI mathematics in October 2026.

## Sources

- [OpenAI — On the Navier–Stokes Millennium Prize Problem (Sep 8, 2026; later revised)](https://openai.com/index/navier-stokes-solution/)
- [OpenAI — Sharing AI progress in mathematics (Oct 6, 2026; updated Oct 15)](https://openai.com/index/sharing-ai-progress-in-mathematics/)
- [GitHub — openai/NavierStokesAndEuler: Lean certificates for the Navier-Stokes and Euler results](https://github.com/openai/NavierStokesAndEuler)
- [GitHub — openai/NavierStokesAndEuler: Comparator challenge statement adapted from Formal Conjectures](https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/NavierStokes.lean)
- [GitHub — google-deepmind/formal-conjectures: Navier-Stokes statement at commit 8bf45ed](https://github.com/google-deepmind/formal-conjectures/blob/8bf45ed70d48b2b2a501de9c00b26bfa38c573ee/FormalConjectures/Millenium/NavierStokes.lean)
- [GitHub — openai/math: release history, withdrawals and formalization count](https://github.com/openai/math/blob/main/history.md)
- [arXiv — Bastounis, Circelli, Hansen: Navier-Stokes lost in translation (Oct 6, 2026)](https://arxiv.org/abs/2610.08144)
- [arXiv — Constantin, Ignatova, Vicol: regularity theorem constraining the force in OpenAI's construction (Sep 17, 2026)](https://arxiv.org/abs/2609.20803)
- [Clay Mathematics Institute — Navier-Stokes announcement (Sep 11, 2026)](https://www.claymath.org/news/navier-stokes-announcement/)
- [Clay Mathematics Institute — Fefferman, official Navier-Stokes problem statement](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf)
- [Clay Mathematics Institute — Millennium Prize rules](https://www.claymath.org/millennium-problems/rules/)
- [Tristan Buckmaster — Statement on the Alpöge-Buckmaster results and contacts with OpenAI (Sep 8, 2026)](https://cims.nyu.edu/~tristanb/statement.pdf)
- [Anthropic — Formalizing Fermat's Last Theorem (Sep 4, 2026)](https://www.anthropic.com/research/formalizing-fermats-last-theorem)
- [AGMAI (IAS) — Responsible Release of AI-Generated Mathematics (Sep 29, 2026)](https://agmai.org/general-sep29/)
- [AGMAI (IAS) — On OpenAI's release of mathematical results (Oct 6, 2026)](https://agmai.org/)
- [Math and AI — Declaration by Fields Medalists (Sep 11, 2026)](https://mathandai.org/)
- [Association for Human Mathematics — Statement on OpenAI's October 6 release](https://www.ahmath.org/statements)
- [Simons Foundation — $15M program with Anthropic and OpenAI for mathematicians (Oct 15, 2026)](https://www.simonsfoundation.org/news/simons-foundation-launches-15m-effort-to-help-mathematicians-navigate-ai-era/)
- [Leo de Moura — Postmortem for kernel soundness bug #14576 (Aug 1, 2026)](https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/)
- [Thomas Hales (guest post on Terence Tao's blog) — What mathematicians should know about the Lean theorem prover (Oct 9, 2026)](https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/)
- [Terence Tao — Open problems mined in a non-renewable fashion (Mathstodon, Sep 8, 2026)](https://mathstodon.xyz/@tao/117237320796901560)
- [Terence Tao — Math 1.0 and Math 2.0 (Mathstodon, Oct 6, 2026)](https://mathstodon.xyz/@tao/117395269325940185)
- [Andreas Thom — Can researchers trust OpenAI with unpublished math? (Mathstodon, Sep 9, 2026)](https://mathstodon.xyz/@andreasthom/117240535270608201)
- [Asaf Karagila — On OpenAI's Partition Principle preprint (Oct 2026)](https://karagila.org/2026/openai-pp/)
- [Asaf Karagila — I don't trust Lean code from AI (Oct 2026)](https://karagila.org/2026/lean/)
- [Scientific American — Did OpenAI solve the wrong Navier-Stokes problem? (Sep 21, 2026)](https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/)
- [Scientific American — OpenAI's blockbuster math proof isn't what you think it is (Oct 13, 2026)](https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/)
- [New Scientist — OpenAI mistranslated mathematics into code for its Navier-Stokes proof (Oct 8, 2026)](https://www.newscientist.com/article/2592824-openai-mistranslated-mathematics-into-code-for-its-navier-stokes-proof/)
- [Fortune — Reactions to OpenAI's release covering more than 370 math problems (Oct 7, 2026)](https://fortune.com/2026/10/07/openai-math-controversy-solutions-370-outstanding-challenges-published-criticisms-celebration/)
- [X — @OpenAI, Navier-Stokes announcement (Sep 8, 2026)](https://x.com/OpenAI/status/2097374640582668336)
- [X — @SebastienBubeck, reply to Levent Alpöge (Sep 8, 2026)](https://x.com/SebastienBubeck/status/2097385316780777529)
- [X — Francesco Maggi on the state of review of the forced Navier-Stokes proof (Oct 10, 2026)](https://x.com/Frances01896069/status/2109010432350376344)
- [X — @danintheory (Dan Roberts, OpenAI), repo update with three withdrawals (Oct 8, 2026)](https://x.com/danintheory/status/2108065033070789090)
- [X — @AnthropicAI, $5M commitment to the Simons mathematics program (Oct 15, 2026)](https://x.com/AnthropicAI/status/2110846112152105136)
- [Polymarket — OpenAI retracts Navier-Stokes solution in 2026?](https://polymarket.com/event/openai-retracts-navier-stokes-solution-in-2026)

---

Canonical: https://www.thedeepfeed.ai/posts/2026-10-17-who-checks-the-proof/
Site: https://www.thedeepfeed.ai
Full corpus: https://www.thedeepfeed.ai/llms-full.txt