# Lean Pool: a formalized mathematics repository grown and maintained by AI agents

> Lean Pool is a living, AI-maintained archive of 211 formalized Lean projects with 837 main results, kept compatible across six dependency upgrades.

- **Source:** [arXiv](https://arxiv.org/abs/2609.25199)
- **Published:** 2026-09-26
- **Permalink:** https://picx.dev/p/10buso
- **Whiteboard:** https://picx.dev/p/10buso/image

## Summary

## 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

| Archive property | Count |
|---|---|
| Completed projects | 211 |
| Lean source files | 7,043 |
| Physical source lines | 3,228,485 |
| Source declaration commands | 193,862 |
| Registered main results | 837 |
| Human / AI / mixed projects | 70 / 102 / 39 |
| Commit contributors | 18 |
| Contributors with merged PRs | 17 |
| Community PRs merged | 63 |

### Dependency Upgrade Results

| From Lean | To Lean | Projects at probe | Compiler failures |
|---|---|---|---|
| 4.30.0-rc2 | 4.31.0-rc1 | 59 | 44 |
| 4.31.0-rc1 | 4.32.0-rc1 | 91 | 58 |
| 4.32.0-rc1 | 4.33.0-rc1 | 143 | 100 |
| 4.33.0-rc1 | 4.33.0-rc2 | 145 | 19 |
| 4.33.0-rc2 | 4.34.0-rc1 | 148 | 3 |
| 4.34.0-rc1 | 4.34.0 | 191 | 97 |

### Optimization Results

| Accepted change | Lines removed | Build min ↓ before → after | RAM GiB ↓ before → after |
|---|---|---|---|
| 117 Proof-search simplification | 511 | 5.30 → 5.25 (+1.1%) | 15.6 → 15.6 |
| 187 Library-wide compression | 45,217 | 16.11 → 15.59 (+3.3%) | 26.1 → 26.9 |
| 246 Contributor proof golfing | 12,515 | 21.83 → 23.01 (-5.4%) | 25.9 → 24.6 |
| 338 Certificate simplification | 513 | 30.22 → 29.13 (+3.6%) | 21.0 → 20.9 |
| 339 Elaboration-cost reduction | 54,965 | 28.46 → 26.82 (+5.8%) | 19.8 → 19.6 |

### Project-Level Optimizations

| Accepted change | Net lines removed | Project seconds ↓ |
|---|---|---|
| Tactic-import cleanup | 735 | — |
| Restricted-sum proofs | 65 | 20.01 → 18.45 |
| Navier-Stokes reusable APIs | — | 879.67 → 887.78 |
| Infinite Connes rigidity | -31 | 118.00 → 93.70 |
| Burkholder majorant proofs | 1,064 | 23.84 → 19.35 |
| Quantum parallel repetition | 32 | 141.85 → 86.08 |
| Interior-point LP proofs | 249 | 13.98 → 10.69 |

### Review Service Pricing

| Price basis | Reports | Total | Median |
|---|---|---|---|
| Historical API estimates | 285 | $308.52 | $0.20 |
| Codex API-equivalent estimates | 6 | $752.38 | $89.03 |

### Exposition Coverage

| Exposition coverage | Count |
|---|---|
| Documented projects | 203 |
| Source declarations | 173,362 |
| Theorems and lemmas | 124,412 |
| Dependency links | 1,389,967 |
| Declarations used by multiple others | 87,408 |

### 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."*

---

_Markdown view of https://picx.dev/p/10buso, served by PicX — AI-generated visual whiteboard summaries of research papers._