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
Each conjecture formalization lives in its own repository, included here as a git submodule. To clone everything:
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 |
| Legendre | Number Theory | legendre-conjecture |
| Oppermann | Number Theory | oppermann-conjecture |
| Strong Goldbach | Number Theory | goldbach-conjecture |
| Twin Prime | Number Theory | twin-prime-conjecture |
| 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.