The Lean research ecosystem, in one directory.

A collaborative formalization of results around the Polynomial Freiman-Ruzsa conjecture in additive combinatorics.

A formal proof of Carleson's theorem on almost-everywhere convergence of Fourier series.

Formalized additive-combinatorics results on almost periodicity and arithmetic progressions.

A formal development of the Prime Number Theorem and related results in analytic number theory.

A large collaborative project formalizing the mathematics needed to prove Fermat's Last Theorem.

A formal proof of Fermat's Last Theorem for regular prime exponents.

A Lean development of local and global class field theory and its algebraic foundations.

A formalization of toric geometry, including fans, cones, and the varieties they define.

A formal study of exceptional triples related to the $abc$ conjecture.

A probability-theory development constructing and studying Brownian motion in Lean.

A completed proof of a theorem implying that an immersed sphere $S^2 \subset \mathbb{R}^3$ can be turned inside out by a regular homotopy.

A formal library for higher category theory and infinity-cosmoi.

A formalization project for the optimal sphere-packing theorem in eight dimensions.

A standalone formalization of spectral-theorem results for operators.

A combinatorial route to Brouwer's fixed-point theorem and the existence of mixed Nash equilibria.

A collaborative classification of implications between single-operation equational laws.

A broad formal library of results and exercises in modern combinatorics.

A formalization project around Seymour-style decomposition results in combinatorics.