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.
1,000The following resolve YES:
Prime gap (Axiom and IIRC also OpenAI)
Fermat's Last Theorem (Anthropic)
Navier-Stokes (OpenAI)
Pi is transcendental: https://github.com/samuelborza/IsTranscendentalPi
Independence of parallel postulate: https://leanprover.github.io/lean-eval-leaderboard/problems/parallel_postulate_independent/
Pick's theorem: GitHub - Dronmong/Formalizing-Pick-s-Theorem-in-Lean: An ongoing Lean 4 formalization of Pick's theorem via lattice geometry and shoelace identities.
Platonic solids: https://leanprover.github.io/lean-eval-leaderboard/problems/platonic_classification/
and there is probably more