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.
If his proof is validated as correct, resolves to that option regardless of any intermediate mistakes, bugs, or drama along the way.
If not, resolves to the option that most closely describes the primary and most basic failure mode of his Lean proof.
Market extends if still under serious review.
---- AI UPDATES BELOW ----
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
Update 2025-12-31 (PST) (AI summary of creator comment): If David Budden releases the proof in multiple parts (e.g., "part 1", "part 2", etc.) and fails to release all parts by the deadline, the market will resolve to "No proof released" since partial snippets don't count.
Update 2026-01-05 (PST) (AI summary of creator comment): If the proof compiles using sorry or axioms with a formalization which has been documented as critically flawed, the market will resolve to "Wrong problem / formalization error" rather than "Incomplete proof", because the formalization issues take precedence when they are already documented.
1,000People are also trading
So it turns out that the formalization on Lean-Dojo, which Budden was working on proving, is itself not considered reliable:
https://x.com/ElliotGlazer/status/2008014435189952825?s=20
There currently is no good Lean formalization of NS.
@KJW_01294 Lean-Dojo is just a repository someone set up, not part of Lean. So definitely not "Lean bug".
If he produces a valid proof of the version on LD that would already be quite impressive, but I think it would go under "wrong formalization".
But if it doesn't compile or is incomplete, then those problems dominate
@AhronMaline Proof of LD is likely trivial.
https://github.com/lean-dojo/LeanMillenniumPrizeProblems/issues/4 links to a trivial proof; notably, a LLM could have hidden this exploit (or others like it) anywhere within the full length of the Lean document.
Discussion on https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Budden's.20claims.20about.20Navier.20Stokes/with/566341468 indicates more experienced mathematicians (prompted by all this ruckus) are now working towards a more rigorous formalization at https://github.com/google-deepmind/formal-conjectures/pull/1457
@FastFourier ah, I didn't see that!
Still, it's "trivial" for a human expert, after noticing the flaw. I would still be surprised if current LLMs could pull it off
@AhronMaline In any case, at least right now, there is definitely a formalization error?
@creator The Lean Dojo formulation (which Budden based his proof on) seems to be invalid. If that's true and the last proof Budden releases is based on current the Lean Dojo formulation, does it resolve to Formulization Error?
@FastFourier right now, Budden hasn't released a supposed proof at all. We don't know whether he will, and if so, whether it will use that wrong formalization
@FastFourier Yes, if: 1) he publishes a full proof that compiles, and 2) it's based on the flawed LeanDojo formalization it should resolve "Wrong problem / formalization error"
@AhronMaline Yeah, I figured I'd ask just to clarify in contrast to earlier note that incomplete proof could hold priority over wrong formalization since the latter is normally harder to evaluate
@FastFourier so from Simon's answer, that still holds. It's only "formalization error" if the proof is complete
@FastFourier Yeah, but now that for this case the formalisation issues would have already been documented, they should take precedence over “incomplete proof” as I initially suggested
@AhronMaline Yes, right now it would still resolve “No proof”
@Simon74fe Oh, then I misread your response.
So now:
Doesn't compile -> no proof, no matter what formalization
Compiles using sorry or axioms, with a new formalization -> incomplete proof
Compiles using sorry with LD formalization (or another one already known to be wrong?) ->wrong problem
Is this right?
@KJW_01294 Good point. I have removed the bet from the market description. If he drops a lean proof before market close and the proof is accepted as correct by the mathematical community at any point it should still count!
This was in the initial market description:
If his proof is validated as correct, resolves to that option regardless of any intermediate mistakes, bugs, or drama along the way.
https://x.com/davidmbudden/status/2008010372222218740
I just want to point out, this market gives me another 30 days :)
60% of you are going to be aggrieved to learn that I used this for the problem formulation haha
https://github.com/lean-dojo/LeanMillenniumPrizeProblems/tree/main/Problems/NavierStokes
https://github.com/lean-dojo/LeanMillenniumPrizeProblems
Lean Dojo already has a formulation by 3rd party and should be trustworthy, and I'm pretty sure he said his proof would be using the Lean Dojo formalization. Also, it's fairly easy to validate what axioms a theorem uses in Lean.
The ns-lite.lean that was supposed to be a preview of the proof structure has a lot more content and like 10 parts to it, a lot of which I'm guessing would need to be filled out with more details, whereas part 1 of the full proof that was dropped yesterday barely gets started.
I still think the most likely way this resolves against Budden is lack of a proof entirely.
@FastFourier Never mind - https://x.com/ElliotGlazer/status/2008014435189952825
Lean Dojo is not reliable.
Far be it from me to influence resolution criteria. But I only just started uploading the proof now :) https://x.com/davidmbudden/status/2006140494410309933?s=20
@DavidBudden The paper claims that a geometric decomposition of space forces viscosity to dominate vortex stretching, implying global smoothness of 3D Navier–Stokes flows. - done? we have a proove?
@KyleY This is "part 1". If he doesn't release all the other parts it would resolve "No proof" (partial snippets don't count)
@Simon74fe gotcha, ok that updates my assumptions because his last tweet implies he’s trying to rework everything
@Simon74fe but for clarity, if the rest of his parts are based on this part 1 that will be “wrong problem” unless something very very surprising happens or part 1 is actually irrelevant to the rest, no?
@KyleY It depends on what he does in the other parts. Hypothetically, the other parts could indeed try to solve the real claim and part 1 is just something he uses in these other parts?
But if he releases the other parts, and the other parts also don't try to prove the claim, then it would indeed resolve as "wrong problem"