All formalizations.

Libraries

Cluster algebras

A Lean formalization of cluster algebras.

Website Lean Blog post

The Stacks Project

A Lean formalization of the Stacks Project.

Website Lean Blog post

The classification of finite simple groups

A Lean formalization of the Classification of Finite Simple Groups.

Website Lean Blog post

Bounded gaps between primes

A Lean formalization of bounded gaps between primes.

MathEconLib

A shared formal foundation in Lean 4 for research and applications in economics, co-founded by academic economists and Axiom Math in 2026.

Formalizations of community work

Nov 2026

The smallest-parts function and elliptic curves

Ajit Singh

Nov 2026

Ramanujan-type congruences for the smallest parts function

Larry Rolen

Oct 2026

On sign patterns of Fourier coefficients of theta quotients

Koustav Banerjee, Kathrin Bringmann, Bernhard Heim, Ben Kane

Oct 2026

Class polynomial obstructions to canonical congruences for the smallest parts function

Larry Rolen

Sep 2026

A new proof that more than 2/3 of the zeros of the Riemann zeta function are simple and on the critical line

Youness Lamzouri

Jun 2026

Dominant Zeros of Nekrasov–Okounkov Polynomials

Bernhard Heim, Markus Neuhauser

Apr 2026

A quadratic form generalization of rational dinv

Yifeng Huang

Journal arXiv Lean