openai/NavierStokesAndEuler: A Lean Certificate Proves the Logic and Leaves the Authorship Blank

The repository holding the formal verification for OpenAI's Navier-Stokes result ships an Apache license with the copyright line still unfilled. That is a small detail on a repo whose entire controversy is about who owns the work.

The repository is two days old, sits at Trendshift's number five slot, and holds Lean 4 formalizations accompanying OpenAI's finite-time blowup results for Navier-Stokes and Euler. Roughly 1,600 stars. No releases. Apache 2.0.

Open the LICENSE file and it reads, in the copyright notice at the bottom of the Apache template:

Copyright [yyyy] [name of copyright owner]

The brackets are still there. Nobody filled them in.

On most repositories that is a shrug. Somebody ran a scaffold, the placeholder survived review, it gets fixed in a week. On this repository it is close to poetry, because the single loudest argument in mathematics this week is precisely the question of whose name goes on this work.

What the certificate actually certifies

Formal verification in Lean is a real thing and I do not want to undersell it. A Lean proof term either type-checks against a stated theorem or it does not. There is no persuasion involved, no referee's judgment, no "the argument in section four is a bit thin." The kernel accepts it or rejects it. For a domain where a 100-page PDE argument can hide an error for years, that is genuinely valuable.

But the guarantee has an exact shape, and the shape matters. A Lean formalization proves that a proof term satisfies a given statement in a specified formal system. It does not prove that the formal statement is the theorem the manuscript claims.

The anonymous Belgian mathematician who wrote the September 10 response to all this puts the gap cleanly. You still have to verify that the formal statement corresponds to the announced theorem, that the notions of regularity, compact support, and solution are faithfully represented, and that the results accepted as premises are correctly identified. A formal proof can establish something slightly different from what the reader believes they are looking at, if the translation between ordinary mathematical language and formal language is not examined carefully.

So the certificate moves the hard part rather than removing it. Before Lean, the risk was a subtle error buried in a long argument. After Lean, the risk is a mismatch between the informal statement and the formal one, plus whatever is hiding in the premises you accepted. That second risk is smaller and much more localized, which is why formalization is progress. It is not zero, and treating a green kernel check as the end of the conversation is the mistake this repository invites.

Tristan Buckmaster, who is at the center of the dispute, made the same point in the other direction and against his own interest. He and Levent Alpöge withheld their hypo-dissipative Navier-Stokes result specifically because the Lean verification had not finished, and in his email to OpenAI he wrote that they intentionally decided against rushing out a Lean certificate alongside an unpolished preprint, because the first thing anyone reads should be a mathematical argument presented in the normal manner rather than just a formal certificate.

He is describing the certificate as insufficient in a case where he had one coming.

The blank line is not just an oversight

Here is what makes the empty copyright field more than a lint error.

OpenAI's published manuscript for the Navier-Stokes result lists exactly one author: "OPENAI." Not a team. Not a lead researcher with a lab affiliation. An institution.

The Belgian response identifies the problem with that, and it is a practical one rather than a matter of etiquette. Someone chose the problem. Someone determined which directions to explore. Someone organized the agent runs, selected the relevant outputs, checked for errors, and decided on the theorem's final form. A single institutional author makes all of those contributions indistinguishable from each other and from the model's.

It also leaves open a question with teeth: who responds when a specialist challenges a lemma, an estimate, or the correspondence between the printed proof and the formalization? "OPENAI" cannot be asked a follow-up question at a seminar.

So you have a repository whose stated purpose is to make a proof checkable, published under an institutional authorship that makes the human contributions uncheckable, with a license file that declines to name an owner at all. Three layers of the same evasion, and only one of them is an accident.

What Buckmaster's statement adds, and what it carefully does not

Buckmaster published a signed statement that reached wide circulation on September 10. It is worth reading in full rather than through anyone's summary, including mine.

The parts he asserts as fact about his own work: he and Alpöge released finite-time blowup with smooth forcing for incompressible porous media, Boussinesq, and 3D incompressible Euler. The program was not started by them and was not proposed by a language model. Credit for the basic idea goes to Diego Córdoba and Luis Martínez-Zoroa, who spent several years exploring forced blowups, and Buckmaster writes that in his view Martínez-Zoroa deserves a Fields Medal for opening the direction. Their contribution was pushing that program from rough forcing to smooth forcing and to Euler, with heavy LLM assistance. He describes the first LLM-generated proof Alpöge sent him as the most horrendous he has ever read, verified in Lean on August 22, and calls the Euler write-up "AI slop" in his own words, apologizing for it.

The parts he reports as what he was told: on September 6 calls, that an internal OpenAI model had produced a roughly 100-page proof of finite-time blowup for forced Navier-Stokes, corresponding to options (c) and (d) in Fefferman's Clay problem statement. That he was shown a prompt and told the model had simply been given the problem statement. That during the call, as team members sent corrections into internal chat, it emerged an entire team had worked on it, that easier problems including Euler were tried first, and that the prompt shown to him had itself been written by prompting Codex. That two arrangements were proposed to him, one of which removed Alpöge from authorship, with Alpöge's employment at Anthropic given as the reason.

And the parts he explicitly refuses to claim, which are the ones a summary usually eats: he has not seen OpenAI's proof. He does not know what the model did or how. He does not know whether their data was used. He states, in his own words, that he is not accusing anyone of anything.

A secondhand report has Sébastien Bubeck calling the accusations false and inflammatory with a fuller response promised. I could not verify that against a statement from Bubeck himself while writing this, so treat it as a reported denial rather than a quoted one.

What is left after all the hedging is still substantial, and it is structural rather than personal. Buckmaster asked directly whether the model had been trained on, or had access to, their Codex sessions, into which they had been putting all their drafts for the whole project. He says he was told the model did not look up user data, asked again specifically about training, and did not get an answer.

Put this into practice

You are not going to prove a Millennium Prize problem this quarter. The transferable parts are smaller and they apply to anyone shipping work through a vendor's agent.

Read the LICENSE file text, not the badge. Cache-busted raw file text, not the rendered GitHub page, which serves stale content. An unfilled Apache template with [name of copyright owner] still in it is not a valid grant from a named party, and on a repository from a large organization it usually means nobody in legal looked at it. That does not make the code unusable, but it does mean your reuse rights rest on an assumption rather than a statement.

Treat a formal certificate as a claim about a formal statement. When something ships with a proof, a fuzz corpus, a type-checked spec, or a verified build, write down the exact statement that was verified and check it against the thing you actually care about. The certificate is evidence about the middle of the chain, not about the ends.

Ask who signs. If an artifact is published under an organization name with no individual attached, you have no one to ask a follow-up question and no one accountable for a defect. That is fine for a marketing page and a problem for anything you build on.

Find out what your coding agent retains before you paste original work into it. Not the marketing page, the data-retention terms. What is stored, for how long, whether it is used for training by default, and whether zero-data-retention exists on your plan and covers the endpoints you actually use. OpenAI's Astra announcement notes that Zero Data Retention is available for eligible API customers on supported endpoints, subject to approval, which is three qualifiers on one sentence and worth reading as three separate questions. Do this for whichever vendor you use; the point is the habit, not the vendor.

Keep a local record of your own timeline. Dated commits, dated notes, drafts in version control you own. Buckmaster was able to write a statement with specific dates attached because he had them. The single cheapest insurance against a priority dispute is being the party who can produce a chronology.

Honest limitations

This is one side of a live dispute and the other side has said it will respond. Nothing here establishes that anyone's data was used improperly, and Buckmaster himself declines to claim it. A proof can be entirely correct and produced under questionable conditions, and a controversy about the conditions is not an argument against the theorem. Those two assessments have to be run separately and I am only competent to comment on one of them.

I have not read the Lean formalization. I cannot evaluate whether the formal statement matches the manuscript's theorem, which is precisely the gap this article is about, and it would be dishonest to pretend otherwise. The people who can evaluate that are a small number of PDE specialists who also read Lean, and their verdict has not arrived yet.

I could not do a second verification pass on this repository's figures. The star count, the release status, the license text, and the default branch all come from a single cache-busted read this morning. The star count in particular moves fast on a repo two days old and will be wrong by the time you read this.

The ten-million-dollar compute figure that keeps circulating, corresponding to 300 billion tokens generated in eight days by ten thousand agents, appears in the Belgian response as a number being passed around in the discussion rather than as a figure OpenAI published. I have not seen a primary source for it and neither, as far as I can tell, has the person quoting it.

What to do with this

The interesting thing here is not who behaved badly. It is that formal verification arrived as the answer to "how do we trust AI-generated proofs," got adopted almost immediately, and turned out to answer a narrower question than the one everybody was asking.

That pattern is going to repeat everywhere agents produce artifacts humans cannot review at speed. Type-checked specifications, verified builds, signed attestations, formal policy proofs. Each one will be a genuine improvement and each one will settle the mechanical question while leaving the specification question and the attribution question exactly where they were.

Go look at the last thing an agent produced for you that shipped with some kind of green checkmark. Write down, in one sentence, what that checkmark actually asserts. Then write down what you have been assuming it asserts.

If those two sentences match, you are fine. If they do not, that gap is where your next incident lives, and it will not be the checkmark's fault.

Sources: openai/NavierStokesAndEuler, Tristan Buckmaster's statement, "Navier-Stokes, AI and the future of research in mathematics", GPT-6 Astra announcement.

Medium metadata

Title: openai/NavierStokesAndEuler: A Lean Certificate Proves the Logic and Leaves the Authorship Blank
Subtitle: The repository holding the formal verification for OpenAI's Navier-Stokes result ships an Apache license with the copyright line still unfilled.
Tags: OpenAI, Formal Verification, Lean, AI Ethics, Mathematics
Canonical: import from the fervorai.dev URL