Which theorems will be formally proven in Lean by the end of 2028?
20
325Ṁ755
2028
96%
Pi is Transcendental
95%
The Independence of the Parallel Postulate
94%
The Number of Platonic Solids
90%
Pick's theorem
71%
The Four Color Theorem
63%
Fermat’s Last Theorem
52%
Jordan–Brouwer separation theorem
50%
15 and 290 Theorems
50%
Kuratowski's theorem
23%
Navier–Stokes existence and smoothness (unbounded) counterexample
20%
Poincaré conjecture
15%
Hodge conjecture
15%
Navier–Stokes existence and smoothness (unbounded) (positive)

Resolution Criteria

This market resolves YES for each theorem that is formally proven in Lean by December 31, 2028, 11:59 PM UTC. A theorem is considered "formally proven" when a complete, verified proof exists in the Lean theorem prover's main library or in a publicly accessible repository that has been merged or accepted by the Lean community.

Background

Lean is an open-source theorem prover and programming language. It allows mathematicians to formally verify proofs of mathematical theorems using computer assistance. The Lean Mathematical Library (mathlib) is a community-driven effort to formalize mathematics in Lean.

As of 2023, many important theorems have already been formalized in Lean, but several significant results remain unproven in this system. The Lean community maintains a list of "100 missing theorems" that they aim to formalize, and many more theorems are tracked by the 1000+ theorems project.

Further Notes

When posting an open question, please try to indicate whether you are asking about positive or negative resolution. I will seek to resolve ambiguities in the direction of the most plausible single formulation of the theorem at the time of answer creation.

Technology
Math
The Lean Theorem Prover
Get
Ṁ1,000
to start trading!

People are also trading

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will LLMs be able to formally verify non-trivial programs by the end of 2025?
14% chance
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
1% chance
Will an AI implement a full infinity-topos mathematical framework by end of 2025?
5% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
80% chance
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
60% chance
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
74% chance
Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?
61% chance
ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?
46% chance
© Manifold Markets, Inc.•Terms•Privacy