The Kernel Checked the Proof. Who Checked the Question?

Key Takeaways

• OpenAI’s Navier-Stokes release came with a Lean 4 formalization. A proof assistant certifies exactly one thing: that a particular formal statement follows from the axioms. Whether that statement is the Millennium problem is a separate question, and no kernel can answer it.
• In this case the separate question has a good answer. The formal statement was not written by OpenAI. It came from Google DeepMind’s Formal Conjectures project, was reviewed over four months before any proof existed, and has since been examined in public by Lean experts, one of whom wrote that it “is true to the statement of the Clay prize.”
• The trusted part a human must read is one file of 286 lines. Behind it sits a repository of 2,659 Lean files that nobody needs to read.
• What is still unchecked is not correctness. It is understanding. The Clay Mathematics Institute says the problem has “apparently” been settled and that its process is “deliberately unhurried.”
• Verification did not remove the need for human judgment. It compressed it into a smaller place and made that place more important.

On 8 September 2026, OpenAI announced that an internal system had “produced an analytical proof and a Lean formalization that an initially smooth fluid at rest can develop a singularity in a finite time.” The proof is a 166-page paper. The formalization is a public GitHub repository. By OpenAI’s account the agents reached their result after about 88 hours, and the Lean formalization and verification “took an additional 17 hours.”

I wrote two days ago about the argument this set off among Fields medallists. This essay is about a narrower thing: the Lean part. John D. Cook called it the part of Navier-Stokes no one is talking about. Starting from a 2005 estimate by Henk Barendregt and Freek Wiedijk that formalizing one page of an undergraduate textbook takes about a work-week, he put a paper this size at roughly 132,800 person-hours, against OpenAI’s 17. His conclusion: “lowering the cost of anything by four orders of magnitude is revolutionary.”

He is right about the cost. But a cheap certificate is only worth having if you know what it certifies. A commenter under Cook’s post, John Zhang, put the limit in two sentences: formal verification answers “did I implement what I wrote down?” It does not answer “did I write down the right thing?”

So: did they write down the right thing? I went and read the files.

What does a Lean proof actually certify?

Lean is a proof assistant. You state a theorem in its formal language, supply a proof, and a small program called the kernel checks every inference. If the kernel accepts, the statement follows from the axioms. That is the whole guarantee. It is a strong one, and it says nothing about what the statement means.

This matters because a formal statement is a translation. The Millennium problem is defined by a six-page description written by Charles Fefferman in ordinary mathematical prose. Fefferman wrote that, “to give reasonable leeway to solvers while retaining the heart of the problem, we ask for a proof of one of the following four statements”: existence and smoothness on three-dimensional space (A) or on the periodic torus (B), or breakdown in either setting (C, D). OpenAI claims C and D. In Fefferman’s wording, C asks for a smooth, divergence-free initial velocity and a smooth, rapidly decaying external force for which no smooth solution with bounded energy exists for all time.

Turning that paragraph into Lean means making choices. How do you say that a function is smooth on a region that includes its boundary at time zero? What is the derivative of a function at a point where it has none? Lean’s mathematical library answers the second question with a convention: the derivative is defined to be zero there. The statement file says so in its own comments, noting that its divergence operator “has the corresponding junk value” of zero when the field is not differentiable. Conventions like this are harmless when handled with care and can hollow out a theorem when they are not. A proof of a mistranslated statement is still a valid proof, of something else.

Who wrote the formal statement?

Not OpenAI, and that is the most important fact in the repository.

The repository is built around Comparator, a tool from the Lean developers that describes itself as “a trustworthy judge for Lean proofs.” It takes two files. The challenge file contains the theorem statement with its proof left as sorry, Lean’s placeholder for “not proved yet.” The solution file is the submission. If Comparator succeeds, its documentation says the listed theorems are guaranteed to “prove the same statement as provided in Challenge,” to “use no more axioms than listed,” and to “be accepted by the Lean kernel.” Eric Wieser explained the purpose on the Lean Zulip: Comparator checks that the statement is identical between a trusted and an untrusted file, “such that a human verifying the result must only check the trusted ‘Challenge’ file.”

Here the challenge file is 286 lines and imports nothing but Mathlib. Its header says it was copied from a pinned commit of Google DeepMind’s Formal Conjectures project, a catalogue of open problems stated in Lean. The README thanks that project’s authors for their formalization of the problem statement, “which we adapted for these Comparator challenges.”

The upstream file was written mostly by Tomáš Skřivan, in a pull request opened on 3 January 2026 and merged on 15 May, after 37 review comments from several reviewers. The version OpenAI pinned dates from 27 July. OpenAI says its effort began on 1 September. So the target was fixed, in public, by someone with no stake in the outcome, before anyone aimed at it.

Good provenance does not make a statement right. Skřivan’s own pull request listed his doubts: “at various places I’m not completely sure if there should be t ≥ 0 or t > 0 as fderiv might not give what we think at t=0.” And when the proof landed, he wrote on the Lean Zulip: “Which I wrote mostly :) It got looked over by couple of actual mathematicians but at this point it deserves a bigger scrutiny.”

Who checked it after the proof appeared?

The bigger scrutiny happened in that thread over about three days.

The re-run. Within a day of the release, a user named Sebastián Rodrigo built the repository and ran Comparator himself: “It compiles with three standard axioms.” The configuration permits exactly three: propext, Quot.sound and Classical.choice. The configuration also turns on a second kernel, nanoda, which re-checks the proof alongside Lean’s built-in one. The repository’s metadata reports a sorry_count of 0.

The diff. “Almost a copy” is not the same as a copy, so Mirek Olšák published the exact differences between OpenAI’s challenge file and the Formal Conjectures original, and Felix Pernegger went through them one by one: changed imports, a changed namespace, removed cataloguing attributes, statements A and B dropped, notation made local. His summary: the “relevant Lean declarations are identical (‘syntactically’),” and every difference is cosmetic.

The translation. A user named Bilal raised the real question. Fefferman states the decay condition on the force as bounds on every mixed partial derivative in space and time. The Lean file bounds the norm of a single higher-order derivative object instead. “Comparator can verify the Lean theorem, but it doesn’t by itself tell us that this formal encoding is exactly equivalent to Clay’s intended condition.” Skřivan’s reply: “This is a very good point and probably the largest divergence I’m aware of,” though he had reasoned that the two are equivalent because all norms on a finite-dimensional space are. Jason Rute listed “community agreement that the statement is correct” as the first thing still missing, adding that Formal Conjectures “has had mistakes.”

The answer. On 11 September, Sébastien Gouëzel, a Mathlib contributor whom the next poster described as more authoritative than himself, replied: “If the question is mathematical, I can answer: the formalized statement is true to the statement of the Clay prize, so getting a Lean proof for this formalized statement is all that is needed.” Luigi Massacci then wrote what he called “a more slavishly faithful formalization of the official clay statement,” with partial derivatives spelled out coordinate by coordinate as Fefferman has them, and reported that it was proved equivalent to the Formal Conjectures version. “I don’t think there is any reasonable doubt over the correctness of the formalization.” Olšák reported a further equivalence with a third, independent formalization from the lean-dojo project. The same day, Formal Conjectures marked C and D as solved, with a link to OpenAI’s first commit.

This is a chat thread, not a referee report. Both equivalence proofs were produced in Lean with an AI assistant, and Olšák noted that one of his runs was not properly sandboxed. But three formalizations written by different people at different times, proved equivalent to one another, are much harder to get wrong in the same way than one. And the judgment that they match Fefferman’s English was made by people qualified to make it.

So, plainly: on the public evidence, the statement holds up. The Lean theorem is Fefferman’s C and D.

One nuance survives. C and D are the forced alternatives. The fluid starts at rest and a smooth external force drives it to blow up. That is squarely within the official problem, which is why a proof of it answers the problem as Fefferman posed it. It is not the same as showing that an unforced fluid can blow up from smooth initial data, which would refute A or B. The Formal Conjectures file still tags A and B as open. A faithful formal statement tells you which question was answered. Knowing which were not is a job for the reader.

What is left to trust?

The kernel. Comparator’s documentation is explicit that its guarantees assume “the Lean kernel is correct.” A second kernel weakens that to the assumption that at least one of the two is. Jay Kruer, in a sceptical essay about what this result means for AI, grants that the Lean rendering “is a straightforward translation defined in terms of battle-tested mathematical objects from Mathlib,” but notes that “soundness bugs have allowed LLMs to launder bogus proofs through the proof kernel before.” On the Zulip, Rute’s view was that with Comparator, “metaprogramming hacks are largely not possible,” that the remaining worry is kernel bugs or unsoundness in the underlying theory, and that he doubts a new one was found and exploited here. He also called his own checklist “overkill,” and gave the reason: “I’m sure Clay and others won’t rest until the proof is understood.”

I have not run any of this myself.

Did OpenAI change the release afterwards?

A small Hacker News post on 11 September was titled “OpenAI changed Navier-Stokes press release and Lean4 code on GH”. Both halves are true. Here is what changed.

The post changed on 10 September, and OpenAI says so in a dated footnote. Comparing the archived 8 September version with the current one, the edits are confined to the “Concurrent work” section. The original said: “While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models.” The revision replaces that with the finding that, “following an investigation,” Tristan Buckmaster’s Codex prompts “could not have influenced the system in any way, including through training.” Nothing about the theorem or the formalization was altered.

The repository has two commits, on 8 and 10 September. The second grew the Navier-Stokes directory from 643 files to 816 and rerouted the last step of both headline theorems so that they now follow from formalized versions of the paper’s Theorem 1.1 and its periodic corollary. The challenge file has exactly one commit in its history. The target did not move.

What did the humans say they checked?

Read the human statements for what each person claims to have verified. The answer is very little, and they say so.

Tristan Buckmaster’s statement is mostly an account of a priority dispute, which OpenAI’s post describes differently and which is not my subject. On the mathematics he is exact about his own position: “I have not seen OpenAI’s proof. I do not know what their model did, or how.” More useful is what he says about his own Lean-verified results with Levent Alpöge: “the first LLM generated proof Levent sent me was the most horrendous I have ever read; we verified it on Lean on August 22nd. Since this point, we have been working around the clock to understand this proof and turn it into something readable.” Verified first, understood later. He had wanted to publish in the opposite order: “the first thing anyone reads should be a mathematical argument presented in the normal manner, rather than just a formal certificate.”

The Clay Mathematics Institute’s statement of 11 September does not mention Lean at all. It says the problem “has apparently been settled,” that the rules “describe the process for evaluating what has been achieved and for assigning credit,” and that “the process is deliberately unhurried.” Its hope is for “waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated.”

OpenAI’s post does not say who, if anyone, reviewed the formal statement. The repository’s metadata lists its review status as “self-assessed.” I have not found a public statement from any mathematician who says they have read and understood the 166-page argument. One may exist.

Where did the thinking go?

In an earlier essay I wrote that a proof is the rare artifact whose validity can be checked without trusting whoever produced it. That is true, and this episode shows its edge. The proof needs no trust. The statement needs a reader. When the Maxwell conjecture fell in July, the model proposed and humans proved. Here the machine proved, and the human contribution shrank to something that looks tiny: 286 lines, drafted mostly by one person in January, argued over by a handful of people in a chat thread in September.

It is not tiny. It is the whole interface between a kernel that understands nothing and a question that, by OpenAI’s count, has been open for roughly ninety years. Everything the certificate is worth flows through that file. The reason it held is that it was written slowly, in public, by someone who listed his own doubts, and reviewed by people who knew the mathematics, all before there was any pressure to make it say something convenient. If the same system had written its own target an hour before proving it, the kernel would have been exactly as satisfied, and the result would deserve far less belief.

That is the pattern to watch as formal verification gets cheap. The thousands of files no one reads are safe to ignore. The one file someone must read is where the judgment lives: what was asked, what was assumed, what was left out. Verification did not remove the need for human thinking. It moved it upstream, to the question, and downstream, to the understanding that Clay is prepared to wait for. The middle is the part we were able to hand over.

Every quotation above comes from the linked source: OpenAI’s post and repository, the Clay statement, Fefferman’s problem description, Buckmaster’s statement, the posts by Cook and Kruer, the Formal Conjectures history, and the public Lean Zulip thread. Nothing here is quoted from memory, and I did not run the Lean code.