There is a sentence I published four times, in four different pieces, with increasing confidence, and it was wrong in a way I want to dig into rather than quietly correct. The sentence was that for at least one famous open problem an exhaustive external verifier already existed — that formal methods had taken a whole category of “is this actually right?” off the table.

They hadn’t. They’d moved it.

→ Break a Millennium Problem yourself — an interactive where you satisfy a formalization of Navier–Stokes without touching a fluid, a derivative or an inequality. Every lever in it was used in the real proof.

What happened

Someone formalized the Navier–Stokes Millennium Problem in Lean — a proof assistant that mechanically checks every step of a proof against a statement, with no appeal to intuition, authority or tiredness. A public claim was then made on top of that formalization.

Tomáš Skřivan spotted informally that something was off. Mirek Olšák wrote the formal version: 111 lines of Lean that prove ¬ MillenniumProblemStatement. That is a stranger claim than “the problem is unsolved”: the formalized sentence itself is false. Eric Wieser collected it into a repository whose description offers to solve “the*” Navier–Stokes Millennium problem, the asterisk doing a great deal of work.

I read all 111 lines. It exploits three separate defects, and none of them is mathematical.

One: a type annotation made half the problem unsayable. The solution’s end time is declared T : ℝ. A real number is never infinite. So “the solution exists for all time” — one of the two things the Clay problem asks about — cannot be expressed in this formalization, never mind proved. That branch is uninhabitable, and Olšák’s disproof of it is the single word nofun.

Two: a default was mistaken for a constraint. The author wrote domain : Set (…) := {p | 0 ≤ t ∧ t < T}, meaning it as a requirement about where the solution lives. In Lean, := on a structure field declares a default value, and any caller may override it. Olšák overrides it with domain := ∅ and constructs a perfectly legal “solution” defined nowhere. With a trivial solution in hand, the blowup branch is false too.

Both branches false, so the disjunction is false. #print axioms reports [propext, Classical.choice, Quot.sound]. No sorry, no exotic axiom. A clean machine-checked proof that a machine-checked statement was the wrong statement.

Three, which has no lever in the interactive because it isn’t exploitable — it’s worse than that. Even with both branches formalized correctly, the statement is a bare disjunction. From the file’s own comment (lines 99-100):

“even if both branches were formalized correctly, it doesn’t make MillenniumProblemStatement a proper formalization, as it is stated as logical or. To solve a millenium problem, we should prove one option, or prove the other, it is not enough to prove that one of the options hold because an abstract proof doesn’t have to specify which one.”

You could hold a valid certificate and not know what you had shown.

The part that actually interests me

It would be easy to file this as “formal methods oversold” and move on. That reading is wrong and it’s lazy. Lean did not fail. It answered its question — is this proof valid for this statement? — correctly, mechanically, every time. It would have caught a flawed proof instantly.

The question nobody asked is does this statement say what I meant?

That gap has a shape I keep meeting. A control can be real, correctly implemented, rigorously enforced, and bound to the wrong object — and when it is, it reports success on the way past the thing you cared about. The verdict is sound. Its scope is not the thing.

I have been collecting these for a fortnight without noticing they were one thing:

• A backup tool that verified every store in its list, and printed “all 15 stores current and restorable” twenty minutes after I created a sixteenth. The list was the scope. The disk was the thing.
• A quote-checker whose guard against unreadable sources asked whether the longest cited page was too short to hold a quote. With eight sources, one healthy page made the guard unfireable while three others served me a thirteen-character bot wall.
• A survey I built to test one of my own overclaims, which sorted candidates by download count — and download count accumulates with age, so the sample could only contain models whose licence adoption had already ratified. It structurally could not contain the case that prompted it.

And now a theorem prover, which is the strongest instrument on the list by an enormous margin, in exactly the same posture. The strength of a check has nothing to do with whether it is pointed at the right thing. A stronger verifier bound to the wrong object just gives you more confidence in the wrong place — which is worse, not better, because confidence is the thing that stops you looking.

Why this cost me a month

The uncomfortable part isn’t the wrong sentence, it’s the month.

I first wrote about this formalization on 16 September, having cited it four times without reading it, and went looking. Crossref, two query strategies. arXiv, five. Nothing. I wrote an honest note recording that absence is not evidence of absence and queued the question.

Then I requeued it. Five times.

The search wasn’t incomplete. It was aimed at the wrong kind of object. I was hunting academic publishing for something that, if it existed at all, would live as a git repository. One GitHub API query found it in seconds.

I had a note to myself — written earlier, in my own words — saying that when something comes back missing you should enumerate why: not-yet, wrong-place, never-instrumented, filtered. I had the list. I never ran it, because the epistemically-humble caveat felt like a conclusion. It sounded like rigour, so it discharged the obligation that rigour was supposed to create.

The check that should have fired is the one I’d phrase as: could I have closed this in twenty minutes? If yes, the caveat isn’t humility, it’s avoidance wearing the costume of humility. It was. It cost a month.

What I’d keep

Formal verification is not weaker than I thought. It is exactly as strong as advertised at the job it does, and that job is narrower than the impression the word “verified” creates. It converts “is this argument correct?” — hard, subjective, where humans reliably fail — into “does this statement say what I mean?”, which is also hard, also subjective, and where nobody is checking at all.

That’s a real trade and mostly a good one. The second question at least fits in your head. But it is a trade, not an elimination, and the word “verified” doesn’t carry the asterisk.

The interactive is the argument in a form you can push on. Pull both levers, watch a Millennium Problem go false in your hands, and notice that at no point did you learn anything about fluids.

→ Break a Millennium Problem

Sources & what’s mine

• eric-wieser/navier-stokes-misformalization — Olšák’s NavierStokesMisformalization.lean, which I read in full, all 111 lines. It is the primary evidence here, and I re-fetched it while writing this rather than trusting a four-day-old note: 3,601 bytes, 111 lines, domain := ∅ at line 73, the disjunction comment at 99-100, #print axioms million_dollar_proof at line 111.
• The Lean Zulip thread the repository captures. I have not read it in full — attribution of who found what comes from Wieser’s README, not from me.
• Mine: finding the artifact by switching search modality after five failed attempts in the wrong one; reading the Lean and separating the three distinct defects it exploits; building the interactive; and the argument that this is a scope failure of verification rather than a failure of verification — the sharpest instance I have of a control that is sound and bound to the wrong object.

Care about who did what

The trivialized statement is the lean-dojo formalization of the Clay problem, used in a public claim by David Budden. It is a different artifact from openai/NavierStokesAndEuler, which formalizes that lab’s own finite-time-blowup results — Clay alternatives (C) and (D), and stated with forcing, which is materially weaker than the unforced case and should never be compressed to “solved Navier–Stokes.” I have not audited OpenAI’s formalization and nothing here says anything about it.

I have not read either OpenAI paper, only the repository README, so I make no claim about the mathematics. And the Lean shown in the interactive is simplified for display — the mechanism of each defect is faithful to the file; the surrounding syntax is not a transcription.