Formalization targets

[alreadydone]

Wikipedia's list of theorems
Jeremy Tan's 100 theorems
Knill's 272 theorems (being worked on at lean-eval/leanprover by Kim Morrison with Claude)
1000+ theorems
Theorems in my Formal Conjectures List (already moved here)
Missing theorems from Freek Wiedijk's list of 100 theorems (many statements have been formalized)

LeanEval leaderboard and list of tasks
related projects:
FormalQualBench (PhD qualification exam level)
LeanTriathlon : repo, paper, Zulip
FATE (Formal Algebra Theorem Evaluation): repo, paper, blog, news
Formal Frontier, Zulip
Formal Conjectures

Number theory

• equivalence of RH to alternative forms: growth of arithmetic functions, analytic criteria, Jensen-Pólya Program, Li's criterion

Algebraic number theory

• Catalan's conjecture (Mihăilescu's theorem) (in LeanTriathlon)
• Schinzel–Zassenhaus Conjecture (solved by Dimitrov)
• Stark–Heegner theorem

Analytic number theory

• Vinogradov's mean-value theorem
• bounded gaps between primes (Zhang / Maynard)
• Bombieri–Vinogradov theorem, Zulip
• Barban–Davenport–Halberstam theorem
• Siegel-Walfisz theorem, Zulip

Diophantine approximation

• Duffin-Schaeffer conjecture (Koukoulopoulos–Maynard theorem), quantitative version, prior relevant formalization, Mathlib
• Oppenheim conjecture
• Thue–Siegel–Roth theorem
• Schmidt subspace theorem

Transcendence

• Gelfond–Schneider theorem
• Baker's theorem
• Analytic subgroup theorem
• The linear independence of 1, ζ(2), and L(2,χ_{-3})

Arithmetic geometry

• Faltings's theorem (Mordell conjecture): feat(AlgebraicGeometry): function fields and Faltings' theorem leanprover/lean-eval#191

Complex analysis

• Kontorovich's list
• Osgood's lemma, two variable case
• Hartogs's theorem on separate holomorphicity, two variable case
• Yury Kudryashov's several complex variable list
• unbounded denominators conjecture

Lie theory

• Closed subgroup theorem

Algebraic $K$-theory

• Definition of algebraic $K$-theory of rings
• Kurihara (1992) showed that the Kummer–Vandiver conjecture is equivalent to $K_n(\mathbb{Z}) = 0$ whenever $n$ is a multiple of 4.

Spectral geometry

• Selberg's 3/16 bound

Hyperbolic geometry

• Mostow rigidity feat(Geometry): Mostow rigidity, algebraic form leanprover/lean-eval#140
• Margulis superrigidity

Geometry

• disproof of period tiling conjecture, see also
• aperiodic monotile

Symplectic geometry

• the rectangular peg problem, see also

Topology

• classification of simply connected closed 4-manifolds (need singular cohomology, intersection form, Kirby–Siebenmann invariant)

Homotopy theory

• solution of Kervaire invariant one problem

Geometric topology

• define lens spaces
• classification of 3D lens spaces up to homotopy or homeomorphism (proof needs Reidemeister torsion)
• L(5;1) and L(5;2) have same $\pi_1$ and homology but different homotopy type; L(7;1) and L(7;2) have the same homotopy type but are not homeomorphic
• define model geometries and state Perelman's geometrization theorem

Geometric group theory

• statements in Chapter 0 of Farb & Margalit on mapping class groups: feat/chore: move definition of surfaces leanprover/lean-eval#141 + WIP