Summary (Overview)

• Lean Pool is a living archive of formalized mathematics, grown, maintained, and optimized by AI agents, serving as a formal counterpart to arXiv.
• The archive contains 211 completed projects, comprising 3,228,485 lines of Lean code, with 837 registered main results and 18 contributors.
• AI agents handle dependency upgrades (six Lean version bumps completed), library-wide proof shortening, and compilation optimizations, with human oversight ensuring quality.
• The paper documents agent-assisted maintenance restoring compatibility across dependency upgrades, with compiler failures ranging from 3 to 100 projects per upgrade.
• Lean Pool is the most reused external repository in the LeanEval structural audit, demonstrating its value for subsequent research-level formalization.

---

Introduction and Theoretical Foundation

Background

Generative AI has driven recent progress in mathematics, but as generation becomes commodified, verification becomes the bottleneck. Lean has emerged as the primary language for verifying mathematical proofs—both human-made and AI-generated. However, Lean's standard math library, Mathlib, lacks definitions and theorems needed for much of research-level mathematics and grows at a linear rate due to strict human review.

Motivation

AI systems can produce mathematical arguments faster than mathematicians can read them. Formalization makes correctness mechanically checkable while ideas are still being understood. Notable examples include OpenAI's Ten Advances in Mathematics and Theoretical Computer Science and Finite Time Blowup for Navier–Stokes, both released with Lean formalizations [175; 171].

Key Insight

Formalizations become foundations for later research only if they remain compatible with evolving libraries. A reader must find relevant theorems, inspect assumptions, and use them in new developments. Lean Pool addresses this by maintaining completed formalizations together in a common Lean/Mathlib environment.

Admission Rules

Completed projects must:

• Contain no sorry or admit
• Introduce no axioms beyond Classical.choice, propext, and Quot.sound
• Avoid set_option, unchecked declarations, and mechanisms bypassing resource limits
• Include a card identifying authors, upstream source, proof provenance, and main results
• Carry an Apache-2.0 or MIT license

---

Methodology

Growth Mechanisms

1. AI agents discovering formalization projects under permissive licenses and pooling them
2. Human contributors pooling their projects

Pooling involves bumping the Lean version, passing Continuous Integration linters and LLM review, and optimizing hotspots for compilation time and RAM.

Maintenance Workflows

• Dependency-update workflow: Detects new Lean/Mathlib releases, builds the archive, assigns failing projects to repair agents, and assembles patches for review
• Daily jobs: Search for formalizations, inspect open PRs, address maintainer issues, optimize projects, and announce acceptances

Continuous Integration

CI combines:

• Full-library build
• Warning checks
• Mathlib's declaration and source-style linters
• Archive-specific quality gates (project cards, attribution, allowed axioms, proof/file sizes)
• Compiled-environment audit and profiling reports

Mathematical Review

An LLM-based review service examines:

• Faithfulness (statement corresponds to advertised contribution)
• Novelty, significance, sources, and code quality

Documentation

Three types:

1. Traditional Index
2. Exposition (project-level view with dependency graphs)
3. Daily project announcements in Zulip

---

Empirical Validation / Results

Archive Scale

Dependency Upgrade Results

Optimization Results

Project-Level Optimizations

Review Service Pricing

Exposition Coverage

Notable Formalized Results

• Classification of compact surfaces (triangulations to normal forms with boundary)
• Gödel's incompleteness theorems (with arithmetization and provability logic)
• Polynomial Freiman–Ruzsa (entropy-based bounds in additive combinatorics)
• Navier–Stokes and Euler blowup
• Kurosh subgroup development
• Komlós vector-balancing bound and Beck–Fiala discrepancy consequence
• Language generation in the limit (connecting to learning theory)

---

Theoretical and Practical Implications

For Mathematics

• Lean Pool provides a formal analogue of arXiv—a place to quickly share new formalized work with minimal friction
• As formalization becomes easier, most new mathematics papers may acquire accompanying formalizations, with formal dependencies mirroring the dependency graph of mathematical literature

For AI-Assisted Research

• Demonstrates that agent-assisted maintenance can successfully manage large codebases through dependency upgrades
• Shows tradeoffs: proof shortening does not uniformly reduce build time (contributor golfing used less memory but took longer)
• Documents resource demands of large reviews and tradeoffs between reusable interfaces and compilation cost

For the Lean Ecosystem

• Complements existing projects: Mathlib (integrated library), Tau Ceti (AI-authored mathematics), and Palomar Registry (verified separate repositories)
• Lean Pool uniquely maintains independent developments together while preserving attribution and project organization

---

Conclusion

Lean Pool brings completed formalizations into a common environment maintained through agent-assisted upgrades, optimization, review, and community contribution. Its operational history documents repeated successful maintenance, and the LeanEval audit shows reuse in subsequent research-level formalization.

Future Directions

As formalization becomes easier and new math results are immediately formalized upon release, Lean Pool aims to serve as the formal counterpart to arXiv—a low-friction venue for sharing new work while preserving attribution and maintaining dependency usability for later work.

The paper concludes with a vision: "As more mathematical papers acquire formal proofs, the archive provides a place to preserve their attribution and keep their dependencies usable for later work."