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 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 formalization project for the optimal sphere-packing theorem in eight dimensions.

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

A reusable Lean library for automata, languages, and related computer-science proofs.

Shared APIs and formal foundations for computer science, software verification, and certified software in Lean.

Community physics definitions, theorems, calculations, notation, tactics, and quantum-information developments.

A formal library for cryptographic games, probabilistic programs, relational reasoning, and quantitative Hoare logic.

A modular verification framework for interactive oracle reductions and modern zero-knowledge proof systems.

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