Last time I saw someone drop a Lean “proof” of a Millennium Problem it didn’t remotely compile. I hope in this case the error is at least interesting. :)
Isaac King 🔎@IsaacKing314
20 Dec 2025
Update: David claims to have a Lean proof of Navier-stokes, which he is publishing tonight. I have accepted a $10,000 bet that he's mistaken.

Dec 21, 2025 · 1:12 AM UTC

9
2
144
19,560
I regret boosting this…
13
1,489
Sort replies: Relevant Recent Liked
Replying to @JasonRute
an ex-DeepMind researcher getting hit with LLM psychosis is not a good sign for the future
1
14
699
Replying to @JasonRute
well he was a head of research at DeepMind and then he formed his own company
4
633
Replying to @JasonRute
“Doesn’t really compile” is still the right first filter for Millennium Lean drops. Pretty PDFs are not proofs. Before you open a repo, do you check sorry/axioms first, or statement fidelity?
2
Replying to @JasonRute
:) doi.org/10.5281/zenodo.17866…
1
45
Replying to @JasonRute
"It didn't happen last time therefore it definitely isn't happening this time" is not a rational perspective to hold. It might happen, it might not. You don't know until you review it.
295