Proof Wanted

A registry of mathematical theorems and open conjectures awaiting formalization in Lean 4 + Mathlib. Each entry includes a precise mathematical description, a Lean 4 statement that type-checks against current Mathlib (proofs are sorry), and a feasibility assessment.

Candidates

Known Theorems

Candidate	Area	Status	Statement
SL(2,ℝ) trace classification	Hyperbolic Geometry	✅ compiles	Lean
SL(2,ℝ)/SO(2) homogeneous space	Hyperbolic Geometry	✅ compiles	Lean
Cayley transform	Complex Analysis	✅ compiles	Lean
Cantor set Hausdorff dimension	Geometric Measure Theory	✅ compiles	Lean
Besicovitch covering theorem	Geometric Measure Theory	✅ compiles	Lean
Sard's theorem	Differential Topology	✅ compiles	Lean
Coarea formula	Geometric Measure Theory	✅ compiles	Lean
Azuma-Hoeffding inequality	Probability Theory	✅ compiles	Lean
Kolmogorov zero-one law	Probability Theory	✅ compiles	Lean
Poincaré inequality	PDE	✅ compiles	Lean
Lax-Milgram theorem	Functional Analysis	✅ compiles	Lean
Rellich-Kondrachov compactness	PDE	⚠️ partial	Lean
Maximum principle (complex)	Complex Analysis	✅ compiles	Lean
Wasserstein metric	Optimal Transport	✅ compiles	Lean
Kantorovich duality (discrete)	Optimal Transport	✅ compiles	Lean
Optimal coupling existence	Optimal Transport	✅ compiles	Lean

Open Conjectures

Candidate	Area	Status	Statement
Frankl's conjecture (semimodular)	Combinatorics	✅ compiles	Lean
Davenport constant of ℤₙ²	Additive Combinatorics	✅ compiles	Lean
Erdos-Straus conjecture	Number Theory	✅ compiles	Lean
Sunflower conjecture	Combinatorics	✅ compiles	Lean
Chvatal's conjecture	Combinatorics	✅ compiles	Lean
Erdos matching conjecture	Combinatorics	✅ compiles	Lean
Sensitivity conjecture (tight)	Combinatorics	✅ compiles	Lean
Equational theories (samples)	Universal Algebra	✅ compiles	Lean

Status key: ✅ compiles = statement type-checks with sorry proofs against current Mathlib | ⚠️ partial = fallback statement due to missing Mathlib definitions

Building / Verifying

Prerequisites: elan and lake.

git clone https://github.com/MathNetwork/formalization-candidates.git
cd formalization-candidates
lake exe cache get    # download prebuilt Mathlib oleans
lake build SL2RTraceClassification SL2RHomogeneousSpace CayleyTransform \
  CantorSetDimH BesicovitchCovering SardTheorem CoareaFormula \
  AzumaHoeffding Kolmogorov01 PoincareInequality LaxMilgram \
  RellichKondrachov MaximumPrincipleHarmonic WassersteinMetric \
  KantorovichDualityDiscrete OptimalCouplingExistence FranklSemimodular DavenportRankTwo

Each candidate is a separate lean_lib target. Build individually with e.g. lake build SardTheorem.

Repository Structure

├── README.md              # this file
├── CONTRIBUTING.md        # contribution guidelines
├── REPORT.md              # verification report
├── TEMPLATE/              # template for new candidates
│   ├── README.md
│   └── Statement.lean
├── candidates/
│   ├── known-theorems/    # proven results not yet in Lean
│   │   ├── <name>/
│   │   │   ├── README.md
│   │   │   └── Statement.lean
│   │   └── ...
│   └── open-conjectures/  # mathematically unproven
│       ├── <name>/
│       │   ├── README.md
│       │   └── Statement.lean
│       └── ...
├── lakefile.lean
├── lean-toolchain
└── .gitignore

Contributing

See CONTRIBUTING.md. In short:

1. Copy TEMPLATE/ to candidates/known-theorems/<your-candidate>/ or candidates/open-conjectures/<your-candidate>/
2. Fill in the README and Statement.lean
3. Verify it compiles: lake build <YourLibName>
4. Open a PR

Related Projects

• Mathlib4 — the Lean 4 mathematics library
• Lean Zulip — community chat