OpenAI published a massive code repository claiming to solve the Navier-Stokes problem — one of seven unsolved math mysteries that come with a $1 million prize from the Clay Mathematics Institute.
The headlines read like the world had just been cracked open. "OpenAI solves Navier-Stokes." "Millennium problem conquered in code."
The repo is genuinely big. 2,486 files. Real math notation. Real-looking theorems. It's the kind of thing that makes a non-math person go "okay, I trust the machine checked this."
So I read it. Here's what's actually in the box.
First: what "sorry" means when a computer checks your math
Here's a quick primer, because it's the whole story.
Normal math proofs get checked by humans. A mathematician reads your proof and says whether the steps make sense. A proof assistant called Lean works differently: it's a computer that checks every single step for you, and it is extremely literal. If a step is wrong, it tells you and refuses to accept the proof. But if a step is right — if the pieces fit together the way the rules say they should — it accepts it.
Now here's the thing about Lean: it has a built-in keyword called sorry. When you write sorry in a place where a proof should be, Lean says "okay, fine, I'll take your word for it," stamps the box as complete, and moves on. It's like cheating on a test by writing "trust me" in the answer blank. The teacher doesn't reject the paper. The teacher just shrugs and gives you the point, because technically the blank is filled.
Proof engineers use sorry all the time. It's a placeholder — a sticky note that says "I'll fill this in later." That's completely normal in development, like leaving a // TODO in code.
What you don't do — and what this repo did — is ship the "trust me" answers to a $1 million problem and let journalists report the prize has been claimed.
The actual "proof" is the word "sorry"
Okay, here's the heart of it. The repo has two important files where the actual Millennium Problem statements live: ComparatorChallenges/NavierStokes.lean and ComparatorChallenges/Euler.lean. These are the files that formalize what the prize problems are asking.
Here's the entire "proof" of the Navier-Stokes breakdown in the first file:
/- (C) Breakdown of Navier–Stokes solutions on R³. -/ theorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³), InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧ ¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p) := by sorry
That's it. That's the proof. The statement says "there exists a fluid that breaks down, and no smooth global solution exists." And the proof is the word "sorry."
And it's not just one. The periodic version:
theorem navier_stokes_breakdown_periodic (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³), InitialVelocityConditionPeriodic u₀ ∧ ForceConditionPeriodic f ∧ ¬ (∃ v p, NavierStokesExistenceAndSmoothnessPeriodic nu u₀ f v p) := by sorry
The Euler breakdown:
theorem euler_breakdown_R3 : ∃ u₀ : ℝ³ → ℝ³, InitialVelocityConditionDecay u₀ ∧ ¬ (∃ v p, EulerExistenceAndSmoothnessR3 u₀ v p) := by sorry
And the one with the most impressive-sounding statement in the entire repo — a "quantitative singularity" theorem:
theorem exists_compact_smooth_euler_singularity : ∃ (u₀ : ℝ³ → ℝ³) (Tstar : ℝ) (v : ℝ³ → ℝ → ℝ³) (p : ℝ³ → ℝ → ℝ), InitialVelocityConditionDecay u₀ ∧ HasCompactSupport u₀ ∧ u₀ ≠ 0 ∧ 0 < Tstar ∧ Tstar ≤ 1 ∧ ... ∧ ¬ (∃ w q, EulerExistenceAndSmoothnessR3 u₀ w q) := by sorry
Every single theorem that makes the "we solved the Millennium Problem" claim has exactly one word as its proof: sorry.
The other 2,486 files are scaffolding around an empty foundation. Like building a really impressive house around a pile of dirt where the foundation should be.
They literally wrote "OPEN" in the source code
This is the part that should really make your jaw drop.
There's a file called NavierStokes/ProblemStatement.lean. It's the file that defines what "solving" the problem would even mean — what it would take for a real solution to count. And in that file, the authors wrote this in the comments:
candidateStatement is a proposition, not an axiom or a proved theorem. No witness satisfying it is constructed here.
And right next to the main claim, the commented-out definition says:
OPEN: the primary existential content of Candidate Theorem 1.1. There is no proof, witness, or axiom asserting this proposition in this module.
The word is OPEN. They wrote it. In their own source code. In the file that defines the prize problem.
This isn't a mistake. These are mathematicians who know exactly what sorry means and exactly what "OPEN" means. The theorem statements are placeholders waiting to be filled. The claim that Navier-Stokes has been proved in Lean is false, and the people who published this repo knew it was false.
The "ghost" trick: Classical.choice
Okay, so maybe you're thinking: "Fine, the main claims are sorry, but what about the other 2,486 files? Those look real."
And you're right — they are real Lean. They're not gibberish. But there's a trick in how the pieces connect, and it's worth explaining.
At the critical moment in the proof — the moment where they need to actually produce a fluid that has the required behavior, a specific function that satisfies the Navier-Stokes equations and then breaks down — they use a Lean function called Classical.choice.
Here's what Classical.choice does in plain English: you tell it "there exists something with property X," and it hands you back something that has property X — but it doesn't tell you what it is. It's like someone saying "I guarantee there's a coin in this bag," and just... handing you the bag. The coin is in there, or at least something is in there, but you can't name it. You're working with a ghost.
The pattern appears throughout the repo:
noncomputable def actualProfile : ProfileData := Classical.choice profileData_nonempty
This says: "Here is a fluid profile that does what we need. I'm not telling you what it is, but I promise one exists." And then the rest of the repo builds 2,486 files of theorems about this unnamed, unnameable ghost. "If the ghost has property A, then the fluid has property B." "If the ghost has property B and C, then the energy stays bounded." All conditional on something that was never actually shown to exist.
It's like writing a whole mystery novel about a character who lives at 42 Birch Lane, but never showing the house, never showing the character, just saying "trust me, they're there, and here are 2,400 pages about what they would do if they answered the door."
The spreadsheet with no money in the bank
There's a file called ExponentLedger.lean that's presented as the "arithmetic backbone" of the whole construction. It checks whether the exponents in the math work out consistently.
Here's their own description of what it does:
The candidate manuscript, Proposition 10.3, assigns real exponents to analytic estimates. This file checks the arithmetic of those assignments, conditional on the estimates being valid. It does not define the analytic classes, construct a correction, or prove an estimate for a PDE.
"Conditional on the estimates being valid." Translation: "We checked the math, assuming the math is true." Which, yes, is a tautology.
The theorems in the file look like this:
theorem particular_gain_eq {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : particularGain σ κ = 2 / 5 := by unfold particularGain waveExponent apply le_antisymm (min_le_right _ _) simp only [le_min_iff] exact ⟨⟨⟨by linarith, by linarith⟩, by linarith⟩, le_refl _⟩
This is correct. The arithmetic checks out. If σ is at least 1/5 and κ is at most one hundred-thousandth, then this particular gain equals 2/5. No argument.
Here's the problem: across the entire repo, there are 15,375 uses of Lean's arithmetic-checking tools — linarith, ring, and norm_num. Each one proves something like "0 is less than 1/5" or "1/2 minus 3κ is at least 2/5 when κ is small." Individually they're each one line of basic algebra. Together, they create an impression of dense, verified computation. Like a spreadsheet with 15,000 rows of addition that all balance.
But a spreadsheet with no money in the bank is still an empty account.
Why 2,486 files doesn't mean what you think
Big repo. Real code. Math notation. Doesn't mean it contains a proof.
Here's why: if you have one sorry at the bottom, you can build anything on top of it. Add lemmas. Add structures. Add 2,400 theorems about fluid dynamics. Lean will check every single one and say "looks good!" because they're all downstream of the sorry. The sorry is the foundation, and everything above it is load-bearing on that one false premise — or in this case, that one admitted absence.
It's like a house of cards where the bottom card is a sticky note that says "trust me." You can stack a thousand cards on top. They'll all hold. And then one person looks at the foundation and goes "this is a sticky note, not a card," and the whole thing is still just a stack of cards on a sticky note.
What this repo actually formalized:
- What a proof would look like — the shape, the structure, the skeleton
- That the bones are internally consistent — types line up, arithmetic checks out
- That a huge existing math library (Mathlib) is powerful enough to state these ideas cleanly
What this repo did NOT formalize:
- That any actual smooth fluid exists that satisfies the Navier-Stokes equations
- That any actual breakdown or blow-up occurs
- That the ghost from step three (the
Classical.choiceprofile) actually can be built from the equations
And there's one more reason the volume is misleading. Almost every file starts with import Mathlib — which loads a massive, community-built, community-verified library of mathematics that took years of work by professional mathematicians. When you import that, your empty scaffolding suddenly looks like it's standing on the shoulders of giants. The ContDiff definitions, the integral theorems, the measure theory — all real, all verified, all meaningful. It's like importing a credit card with $10 million on it into your budget and saying "I'm rich." The library is real. Your account is still empty.
What a real proof would need to do
For context on what the bar actually is, if someone really wanted to solve Navier-Stokes in Lean, they'd need to:
-
Actually construct a fluid — not just say "a fluid exists," but show the specific function, write out its formula, and prove it satisfies the equations. No ghosts.
-
Prove that fluid exists unconditionally — not from
Classical.choice(the "trust me, it's in the bag" function), but from the actual equations, step by step, with no hand-waving. -
Close the matrix arithmetic exactly — several files involve solving systems of equations where the entries are complicated math expressions. Working in "abstract real numbers" in Lean means you can dodge floating-point problems, but it also means you haven't shown the systems actually have solutions for the real objects you care about. You need either exact precision arithmetic (not approximations) or a verifiable certificate that the machine can check.
-
Delete every
sorry— this one is non-negotiable. Lean has a check that scans a proof and flags anysorryhidden anywhere in its dependencies. A real, publishable proof passes that check. This one does not.
None of the four are present here.
What this actually is
This repo is a formalization of the shape of a proof attempt. It's the architectural blueprint for a house that doesn't exist yet. Not the house. The blueprint.
The authors appear to be formalizing an approach from an unpublished manuscript (they call it "Candidate Theorem 1.1"), and the Lean code is what that proof would look like if the hard parts were filled in. As a research tool? Legitimate. As a "we solved the Millennium Problem" announcement? No.
The problem is the presentation. "OpenAI proves Navier-Stokes in Lean" is what ran in the press. The repo has 2,486 files with real syntax, real imports, and genuinely verified arithmetic lemmas. And at the very bottom, where the proof actually lives, there is a word: sorry.
Lean's willingness to accept sorry is being used — whether on purpose or through sheer disbelief that anyone would care — to mislead people who don't know how proof assistants work. "Lean accepted it" is true. "Lean accepted it with a sorry" means nothing.
A sorry in Lean is not a proof. It's a promise someone made to the machine that they would go back and fill it in. They didn't. The machine didn't ask them to. The machine is a machine.
The Navier-Stokes problem is not solved.