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.