Primary evidence
- Lean Pool: An AI-Maintained Archive of Formalized MathematicsS1 · Primary research · Paper · 2026-09-21
- Lean PoolS1 · Primary research · Repository
Lean Pool publishes an AI-maintained archive for large-scale formalized mathematics
The archive occupies a deliberately different position from Mathlib: it accepts independent completed formalization projects that may not fit Mathlib's tightly integrated library scope, while imposing automated maintenance and quality checks.
What happened?
Lean Pool presents a repository of formalized mathematics that is grown, maintained and optimized with AI agents. The project accepts completed Lean developments that pass repository-wide build, linter, style and proof-integrity gates, supplements deterministic checks with LLM review, and maintains accepted projects against evolving Lean and Mathlib versions. Its separate challenge workflow uses Comparator to compare problem and solution statements and replay proofs through Lean's kernel.
The archive occupies a deliberately different position from Mathlib: it accepts independent completed formalization projects that may not fit Mathlib's tightly integrated library scope, while imposing automated maintenance and quality checks. The public repository reports that project imports are still selected by humans, while AI systems participate materially in review, maintenance and optimization. The corpus size changes continuously and is therefore not treated as a frozen historical claim in this Event.
Why it matters
As AI-generated and AI-assisted Lean projects proliferate, preservation and maintenance become bottlenecks distinct from proving individual theorems. Lean Pool supplies an AI-assisted archival layer between highly curated integrated libraries and loose standalone repositories, making maintenance, search, quality gates and challenge verification part of the AI4Math infrastructure problem.
Significance rationale: Lean Pool is a field milestone in AI-maintained formal-mathematics infrastructure because it turns a large collection of independent Lean developments into an actively maintained archive with deterministic quality gates, LLM-assisted admission review, documentation, semantic search and a kernel-checked challenge workflow. Its significance is the operating model for maintaining formalized mathematics at scale with AI agents rather than a claim that every archived project was discovered or authored by AI.
Historical context
Earlier developments
Later developments
—
Related milestones
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Substantive AI support
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal
- AI contribution
- AI agents materially support repository growth, maintenance, optimization and admission review. The repository explicitly states that projects have so far been selected and added by humans, and many archived formalizations are human-authored, so the archive should not be described as wholly AI-authored mathematics.
- Human contribution
- Human maintainers created the archive, choose candidate projects, define review and quality policies, maintain governance and can intervene in integration work; the project was created at the UW Lean Hackathon by Vasily Ilin and Justin Asher.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-27
Technical details
- Systems
- lean-pool, lean, gpt-6-astra, comparator
- Organizations
- —
- Problems
- —
- Methods
- ai-assisted-maintenance, formal-mathematics-archiving, llm-review, semantic-search, proof-integrity-checking
Sources & artifacts
- Lean Pool: An AI-Maintained Archive of Formalized MathematicsS1 · Primary research · Paper · accessed 2026-09-27
- Lean PoolS1 · Primary research · Repository · accessed 2026-09-27
- lean-pool package record on ReservoirS3 · Independent scholarly · Independent analysis · accessed 2026-09-27
- Lean Pool repositoryArtifact · Code
Verification history
- 2026-09-21 · Paper released · E3 · Inspectable artifact
The arXiv record and public repository establish the archive's stated AI-maintained operating model and expose its CI, review and challenge-verification machinery. Reservoir independently indexes the Lean package and reports build results for repository revisions. These sources corroborate the existence and operation of the infrastructure but do not certify the mathematical semantics or novelty of every project contained in the evolving archive.
Corrections
No corrections recorded.