Lean Pool: An AI-Maintained Archive of Formalized Mathematics

Mathlib grows linearly because every contribution requires human review. Lean Pool is a direct response to that bottleneck: a separate archive of formalized mathematics where AI agents handle the maintenance work that would otherwise queue behind human attention.

The mechanics are worth understanding precisely. Contributions enter through two paths - AI agents discovering permissively licensed formalizations and importing them, or humans submitting their own projects. Either way, admission requires complete proofs with no sorry or admit, no axioms beyond the three standard ones, and a project card documenting authors, provenance, and main results with informal statements. What gets pooled must be serious: complete formalizations of named known results, not partial developments or textbook exercises.

Once inside, the archive is maintained by scheduled agents rather than human maintainers. When Mathlib's version changes, agents bump the dependency, identify failures, generate repair patches, and assemble them for review. The paper's production record of the stable-version migration is instructive: initial repair jobs failed on the graph fundamental-group and incompleteness developments, requiring follow-up integration to resolve API changes around measurability and sigma-finiteness. Agent-assisted maintenance works, but it produces follow-up work.

The optimization record is similarly concrete. Library-wide proof compression, replacement of expensive proof searches, and simplification of computation-heavy certificates have all landed as accepted changes. The before-and-after build measurements show real reductions in elapsed time and peak memory - though contributor golfing in one case used less memory while taking longer, a reminder that proof shortening doesn't uniformly improve compilation.

At the observation point, the archive holds 211 projects comprising over 3.2 million lines of Lean code, with 18 contributors and six completed version bumps. The collection spans Gödel's incompleteness theorems, the polynomial Freiman-Ruzsa theorem, Navier-Stokes blowup, non-sofic groups, and quantum parallel repetition, among others. Lean Pool is also the most reused external repository in the LeanEval structural audit, with matching declarations appearing in more research-level formalization solutions than any other compared repository.

The vision the paper articulates is a formal counterpart to arXiv: new mathematics papers accompanied by maintained formalizations, with formal dependencies mirroring the citation graph of the literature. The LLM-based mathematical review service - which checks faithfulness, novelty, and statement accuracy - has been paused after a redesign, and the paper is candid that its retained reports describe past executions rather than ongoing coverage. That honesty about operational limits is more useful than most infrastructure papers manage.