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 formal study of exceptional triples related to the $abc$ conjecture.

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 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 formalization project around Seymour-style decomposition results in combinatorics.

A Lean implementation of a Lean kernel with formal metatheory. The project documents that it is not a fully independent kernel implementation.

Formal semantics and machine-checked results for the Cedar authorization language, with differential testing against the production implementation.

A completed formalization of the difficult part of the consistency proof for Quine's New Foundations set theory.

A formalization of Harder-Narasimhan filtrations and related results for vector bundles.

LLMs as Copilots for Theorem Proving in Lean