Lean Pool: An AI-Maintained Archive of Formalized Mathematics

As AI systems increasingly contribute to mathematical research, formal proofs make it possible to check arguments before they have been fully examined by mathematicians. Reusing these proofs requires more than preserving their source: formalizations must remain compatible with evolving libraries, and their results must be easy to find and understand. We present Lean Pool, a living archive of mathematical formalizations maintained together as Lean and Mathlib evolve. It combines AI agents, automated checks, and human oversight to maintain independently developed projects while preserving their attribution. We analyze the archive’s contribution and maintenance history, accepted optimizations, mathematical reviews, and evidence of reuse. The operational record shows that agent-assisted maintenance can restore compatibility across dependency upgrades and support library-wide proof shortening and compilation improvements. It also records follow-up repairs after initial automation, the resource demands of large reviews, and tradeoffs between reusable interfaces and compilation cost. Archived mathematics is reused in subsequent research-level formalization. We release the archive, its maintenance workflows, exposition site, and supporting analysis artifacts, aiming to provide a maintained formal counterpart to arXiv.