{"id":"arxiv:2609.25199","kind":"preprint","title":"Lean Pool: An AI-Maintained Archive of Formalized Mathematics","authors":["Vasily Ilin"],"author_count":1,"year":2026,"published":"2026-09-21","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2609.25199","nct_id":null,"source_url":"https://arxiv.org/abs/2609.25199","archive_url":"https://space-kitty.com/papers/arxiv:2609.25199","updated":"2026-09-21","pmid":null,"pmcid":null,"openalex_id":"W7214128504","pdf_url":"https://arxiv.org/pdf/2609.25199","abstract":"Lean Pool is a repository of formalized mathematics. It is grown, maintained and optimized by AI agents.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.AI"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}