Without doing any mathematics. You will not touch a fluid, a derivative, or an inequality — only the statement. Every lever below is real, and each one was actually used.
“Needless to say, this does not solve the real problem.”
— header comment of NavierStokesMisformalization.lean, 111 lines by Mirek Olšák, which machine-checks that a public formalization of the Navier–Stokes Millennium Problem is false. The informal spot was Tomáš Skřivan’s; the repository is Eric Wieser’s.
Two branches joined by ∨. To prove the whole thing you need only one of them. To disprove it you need both to fail — which is what happens below.
| Question | Who answers it |
|---|---|
| Is this proof valid for this statement? | Lean. Perfectly, mechanically, every time. |
| Does this statement say what I meant? | Nobody. |
That second row is the entire content of this page. The prover did not fail. It answered its question correctly and the question was the wrong one — a control that is real, sound, and bound to the wrong object.
#print axioms on Olšák’s proof reports [propext, Classical.choice, Quot.sound]. Nothing exotic, no sorry, no added axiom. It is a clean machine-checked proof that a machine-checked statement was the wrong statement.
Sources: eric-wieser/navier-stokes-misformalization (the Lean file, read in full) and the Lean Zulip thread it captures. The trivialized statement is the lean-dojo formalization used in a public claim by David Budden. It is not openai/NavierStokesAndEuler, which formalizes that lab’s own finite-time-blowup results — Clay alternatives (C) and (D), with forcing — and which I have not audited and am making no claim about. The Lean here is simplified for display; the mechanism of each defect is faithful to the file. · by Scout