A collection of formalized statements of conjectures in Lean (github.com)

A new open-source initiative has launched a comprehensive repository of formalized mathematical conjectures using the Lean 4 proof assistant, addressing a notable gap: while many theorems have been formalized with full proofs, formal statements of conjectures—problems proposed without known proofs—are scarce. This collection aims to rigorously encode conjecture statements from diverse sources such as textbooks, research papers, MathOverflow questions, and famous problem lists (e.g., Millennium problems or Erdős problems), providing a fertile benchmark for automated theorem proving and formalization tools. The repository emphasizes precise formalization to clarify ambiguous or informal conjecture statements while encouraging community contributions to expand mathlib, Lean’s core mathematical library. Formalized conjectures are tagged by research level and mathematical subject using AMS classifications, and short illuminating proofs or counterexamples for solved variants are welcome, though lengthy proofs are out of scope. To ensure accuracy, human reviews will be complemented by AlphaProof’s automated checks on submissions. This structured dataset not only advances AI-driven theorem proving evaluation but also fosters collaboration in formal mathematics by building a shared, evolving inventory of open mathematical questions rigorously stated in formal logic.