Open Conjecture Formalizations
Lean 4 formalizations of open mathematical conjectures, alongside a curated index of notable conjectures transcribed from Wikipedia’s List of Conjectures.
Formalizations
Most existing conjecture formalizations live in standalone repositories and are
included here as git submodules. New formalizations may also be developed
directly in this repository under <field>/<slug>/.
To clone everything (including current submodules):
git clone --recurse-submodules git@github.com:SamuelSchlesinger/open-conjecture-formalizations.git
| Conjecture | Field | Repository |
|---|---|---|
| Agoh–Giuga | Number Theory | agoh-giuga-conjecture |
| Carmichael Totient | Number Theory | carmichael-totient-conjecture |
| Collatz | Number Theory | collatz-conjecture |
| Erdős–Straus | Number Theory | erdos-straus-conjecture |
| Catalan-Mersenne | Number Theory | In-repo directory (number-theory/catalan-mersenne) |
| Legendre | Number Theory | legendre-conjecture |
| New Mersenne | Number Theory | In-repo directory (number-theory/new-mersenne) |
| Oppermann | Number Theory | oppermann-conjecture |
| Fortune | Number Theory | In-repo directory (number-theory/fortune) |
| Strong Goldbach | Number Theory | goldbach-conjecture |
| Twin Prime | Number Theory | twin-prime-conjecture |
| Dittert | Combinatorics | In-repo directory (combinatorics/dittert) |
| Gold Partition | Combinatorics | In-repo directory (combinatorics/gold-partition) |
| Hadamard | Combinatorics | hadamard-conjecture |
| Herzog–Schönheim | Algebra | herzog-schonheim-conjecture |
| Sensitivity | Combinatorics | sensitivity-conjecture |
| Reconstruction | Graph Theory | reconstruction-conjecture |
Conjecture Index
Open Problems
Conjectures that remain unproven, organized by mathematical field:
Up-to-date accounting lives on the field pages:
- Number Theory
- Graph Theory
- Algebra
- Geometry & Topology
- Analysis
- Combinatorics & Order Theory
- Other Fields
Conjectures Now Proved
Conjectures that have been resolved and are now theorems, listed chronologically from 1962 to 2019.
Disproved Conjectures
Conjectures that have been shown to be false via counterexample.
Refutations of Conventional Wisdom
Historical examples of widely-accepted mathematical beliefs that were later shown to be false.
Acknowledgments
This project is developed with AI assistance (Claude by Anthropic). The Lean formalizations, conjecture transcriptions, documentation, site design, CI infrastructure, and repository framework have been produced through human–AI collaboration. All formal proofs are machine-checked by Lean regardless of how they were authored.