No proof released
Doesn't publish a compilable, complete Lean proof by end of January 2026. Teasers, headers, partial snippets, or code that fails to compile don't count.
Incomplete proof (uses sorry/axiom/etc)
Proof compiles but relies on sorry, unproven axiom, missing lemmas, or other placeholders that leave it fundamentally incomplete.
Wrong problem / formalization error
Lean code compiles but formalizes a trivial, different, or already-solved version of Navier-Stokes, or otherwise doesn't correctly represent the intended mathematics.
Mathematical error / other issue
Catch-all for any unexpected failure mode that doesn't fit the other categories.
Lean bug
A bug in Lean's code itself causes the proof to be invalid.
Validated as correct
Accepted by the mathematical community as a correct solution to the Navier-Stokes Millennium Problem. Wins his bet with Marcus Hutter and Isaac King.
If his proof is validated as correct, resolves to that option regardless of any intermediate mistakes, bugs, or drama along the way.
If he loses the bet, resolves to the option that most closely describes the primary and more basic failure mode of his Lean proof.
Market extends if still under serious review.
Update 2025-12-21 (PST) (AI summary of creator comment): If David Budden releases multiple versions of his proof, the best/most complete version will be used for resolution purposes.
Update 2025-12-23 (PST) (AI summary of creator comment): Priority between failure modes clarified:
"Wrong problem / formalization error" takes precedence over "Incomplete proof"
Rationale: Wrong problem statement means the real challenge wasn't even attempted, while incomplete proof means the right challenge was attempted but failed
Use of native_decide that adds an unproven/unsound axiom counts as "Incomplete proof (uses sorry/axiom/etc)"
Update 2025-12-23 (PST) (AI summary of creator comment): Priority clarification for axiom use vs. wrong problem statement:
If a proof uses axioms (e.g., via native_decide) and the problem statement is not verified due to lack of scrutiny, the market will resolve to "Incomplete proof (uses sorry/axiom/etc)"
This is because axiom use is automatically checkable and represents the established failure mode in such cases
Does use of native_decide count as an incomplete proof? What if the proof both has native_decide and the statement is not a correct statement of the problem?
@BoltonBailey Incomplete proof seems like the right category since native_decide adds an axiom. Imo if there are both axioms assumed and questions about the problem statement, the use of axioms should be considered the most "basic failure mode" since that is automatically checkable.
@ElliotGlazer E.g. I think something like this should automatically count as failure by axiom: https://x.com/GanjinZero/status/2002952424991150171
Agree that if native_decide adds an unproven/unsound axiom, that would count as "Incomplete proof (uses sorry/axiom/etc)"
Regarding priority: I would go with "Wrong problem / formalization error" taking precedence over "Incomplete proof". The bet is about solving Navier-Stokes. Wrong problem statement = didn't even attempt the real challenge. Incomplete proof = attempted the right challenge but failed
@Simon74fe Yes native_decide adds the axiom Lean.ofReduceBool, which is considered unsound (its behavior doesn't exactly line up with any classical mathematical proposition).
An issue to consider is that if an axiom is used, most likely scrutiny will end at the identification of this axiom (which is automatic) and little scrutiny will be put in the statement formalization (which requires potentially substantial manual labor).
Case in point, everyone agrees his ns-lite.lean is invalid, but afaict, no one ever bothered to determine if the statement is correct.
@ElliotGlazer Fair point. If axiom use is identified and no one bothers to verify the problem statement, I'll resolve to "Incomplete proof" since that's the established failure.
I guess this is the tweet linking to ns-lite.lean? It seems like this formalization of NSSolution is pretty clearly incorrect because the maps it describes for various physical quantities aren't from 3-dimensional Euclidean space, they're just maps ℝ → ℝ.