Lean Pool: An AI-Maintained Archive of Formalized Mathematics

Summary

Lean Pool is a repository of formalized mathematics described in a 52-page arXiv paper by Vasily Ilin. The archive is grown, maintained, and optimized by AI agents rather than being maintained solely through manual curation. The paper includes six figures and a catalogue of imported projects, presenting Lean Pool as an AI-maintained collection of formalized mathematical work. It is classified under Artificial Intelligence and submitted on September 21, 2026.