Mathlib lacks definitions and theorems needed for research-level mathematics and grows only linearly under strict human review, while AI now generates proofs faster than they can be verified and maintained. Completed formalizations also risk becoming incompatible as Lean and Mathlib evolve.

Lean Pool is a repository of formalized mathematics grown, maintained, and optimized by AI agents. Projects (human, AI, or mixed) are pooled from permissively licensed sources, with cards recording authorship, provenance, and main results. The Lean kernel guarantees proof correctness, while CI linters, an LLM mathematical-review service, and admission rules (no sorry/admit, restricted axioms) uphold quality. Agents perform dependency upgrades, repair broken builds, and apply proof shortening and compilation/memory optimizations.

The archive holds 211 completed projects, 7,043 Lean files, 3.2M source lines, and 837 registered main results (70 human / 102 AI / 39 mixed). Content spans logic, number theory, algebra, analysis, geometry, probability, and CS, including Navier–Stokes/Euler blowup, Gödel incompleteness, and classification of compact surfaces. Dependency-upgrade and optimization workflows repaired failing projects and reduced source size, build time, and memory.