Which theorems will be formally proven in Lean by the end of 2028? | Manifold

Which theorems will be formally proven in Lean by the end of 2028?

8

175Ṁ307

2028

94%

The Number of Platonic Solids

90%

The Independence of the Parallel Postulate

90%

Pick's theorem

57%

Pi is Transcendental

50%

15 and 290 Theorems

38%

The Four Color Problem

34%

Fermat’s Last Theorem

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.

The Lean Theorem Prover

Get

1,000

to start trading!

People are also trading

Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?

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?

Will LLMs be able to formally verify non-trivial programs by the end of 2025?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will fermats last theorem be formalized in lean down to the axiom in 5 years.

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

Will we have a formalized proof of the Modularity theorem by 2029-05-01?

Related questions

Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?

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?

Will LLMs be able to formally verify non-trivial programs by the end of 2025?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Will fermats last theorem be formalized in lean down to the axiom in 5 years.

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

Will we have a formalized proof of the Modularity theorem by 2029-05-01?

© Manifold Markets, Inc.•Terms + Mana-only Terms•Privacy•Rules