Lean Pool: An AI-Maintained Archive of Formalized Mathematics

AI summary

Overview

Research area: Artificial intelligence agents applied to formal mathematical infrastructure — specifically the automated maintenance of a shared Lean/Mathlib library of formalized proofs.

Technical level: Intermediate. The paper is readable without a Lean background because its claims are about repository operations, maintenance statistics, and build measurements, though familiarity with proof assistants, continuous integration, and semantic versioning helps.

Scope: One sentence: Lean Pool describes an archive of 211 completed formalization projects that AI agents import, upgrade, optimize, and document, with the Lean kernel and layered automated review enforcing correctness.

What This Paper Is About

Formal proof verification has become the bottleneck as generative AI makes producing mathematical arguments cheap, and the standard Lean library, Mathlib, grows only at a linear rate because every addition passes strict human review. Lean Pool's goal is to give completed, research-level formalizations a persistent home that keeps compiling as Lean and Mathlib evolve, using AI agents to perform the repetitive maintenance work. The paper documents how the archive is populated, maintained, measured, and reused.

Key Contributions

1. An archive of independently authored formalizations maintained in a common environment. Lean Pool holds 211 completed projects comprising 3,228,485 physical lines of Lean source in 7,043 source files, with attribution preserved per project rather than merged into a single shared mathematical API.

2. Agent-based workflows for growth and maintenance. Daily jobs discover completed formalizations under Apache-2.0 or MIT licenses, prepare attributed imports, review open pull requests, optimize existing projects, and announce accepted results. A separate scheduled workflow detects new Lean/Mathlib releases, probes the archive for breakage, assigns failing projects to repair agents, and assembles their patches.

3. An operational record of dependency migrations and accepted optimizations. The paper reports compiler failures across six Lean version upgrades and measures lines removed, build time, and peak RAM for accepted library-wide and project-level changes.

4. A documentation layer and evidence of reuse. An exposition site covers 203 documented projects with 173,362 source declarations, 124,412 theorems and lemmas, and 1,389,967 dependency links; a separate LeanEval structural audit reports that Lean Pool is the most reused external repository in that audit.

Main Findings

• Admission rules are strict and mechanical. Completed projects must contain no sorry or admit and introduce no axioms beyond Classical.choice, propext, and Quot.sound. They must avoid set_option, unchecked declarations, and mechanisms that bypass the repository's resource limits or linters. Every project requires a card identifying authors, upstream source, proof provenance, and main results, and the source license must be Apache-2.0 or MIT.

• Scale and participation. Lean Pool contains 211 completed projects, 7,043 Lean source files, 3,228,485 physical source lines, 193,862 source declaration commands, and 837 registered main results. Projects split into 70 human-written, 102 AI-written, and 39 mixed. There are 18 commit contributors, 17 contributors with merged PRs, and 63 community PRs merged (excluding the maintainer account).

• Dependency upgrades repeatedly broke large fractions of the archive and were repaired. Under the recorded upgrades: 44 of 59 projects failed compiling from Lean 4.30.0-rc2 to 4.31.0-rc1; 58 of 91 from 4.31.0-rc1 to 4.32.0-rc1; 100 of 143 from 4.32.0-rc1 to 4.33.0-rc1; 19 of 145 from 4.33.0-rc1 to 4.33.0-rc2; 3 of 148 from 4.33.0-rc2 to 4.34.0-rc1; and 97 of 191 from 4.34.0-rc1 to 4.34.0. The archived projects' original upstream Lean environments are listed per project in Appendix H.

• Library-wide optimization changes produced mixed results. Accepted changes removed between 511 and 54,965 lines each. Build time moved from 5.30 to 5.25 minutes (+1.1%) for proof-search simplification, 16.11 to 15.59 (+3.3%) for library-wide compression, 21.83 to 23.01 (-5.4%) for contributor proof golfing, 30.22 to 29.13 (+3.6%) for certificate simplification, and 28.46 to 26.82 (+5.8%) for elaboration-cost reduction. Peak RAM went from 15.6 to 15.6 GiB, 26.1 to 26.9, 25.9 to 24.6, 21.0 to 20.9, and 19.8 to 19.6 GiB respectively. The paper states explicitly that proof shortening does not uniformly reduce build time.

• Project-level optimizations are reported separately. Restricted-sum proofs went from 20.01 to 18.45 seconds (65 net lines removed); Infinite Connes rigidity from 118.00 to 93.70 seconds (-31 lines); Burkholder majorant proofs from 23.84 to 19.35 seconds (1,064 lines); quantum parallel repetition from 141.85 to 86.08 seconds (32 lines); interior-point LP proofs from 13.98 to 10.69 seconds (249 lines). Tactic-import cleanup removed 735 lines with no timing shown, and Navier–Stokes reusable APIs moved from 879.67 to 887.78 seconds while adding interfaces.

• Mathematical review is a distinct service with recorded costs. Retained structured review reports are mostly approvals, grouped by verdict against subsequent PR outcomes (merges and closures). Historical API-based estimates cover 285 reports totaling $308.52 with a $0.20 median; newer Codex API-equivalent estimates cover 6 reports totaling $752.38 with an $89.03 median. The paper notes these equivalent prices are not cash payments and that the service was subsequently redesigned and paused.

• Build cost puts the archive in context. On the same Azure VM, Lean Pool's 3.23 MLOC built in 60.28 minutes using 14.29 CPU hours and 20.03 GiB peak RAM; Mathlib at its matching release (2.33 MLOC) took 37.44 minutes, 9.38 CPU hours, and 7.35 GiB; current Mathlib (2.33 MLOC) took 35.83 minutes, 8.99 CPU hours, and 7.00 GiB; Tau Ceti (1.46 MLOC) took 30.89 minutes, 7.13 CPU hours, and 10.67 GiB.

• The exposition interface exposes formal structure. The deployment covers 203 documented projects with 173,362 source declarations, 124,412 theorems and lemmas, 1,389,967 dependency links, and 87,408 declarations used by multiple others. Per-project graph sizes range from 419 declarations and 1,823 dependencies (language generation in the limit) to 48,626 declarations and 530,547 dependencies (Navier–Stokes and Euler).

• Largest archived developments are predominantly AI- or mixed-provenance. The largest is finite-time breakdown for Navier–Stokes and Euler at 641,073 Lean lines (AI), followed by a complex structure on the six-sphere at 260,646 (AI), classification of Compact Surfaces at 143,423 (AI), polynomial-factor hardness of the closest vector problem at 135,818 (mix), and improved asymptotic bounds for binary and spherical codes at 112,078 (mix). The largest human-provenance entry is Gödel's First and Second Incompleteness Theorems at 55,430 lines.

• Two projects were retired. The forward-Euler and special-numbers projects were removed through a separate curation PR, citing the archive's project-size threshold and the textbook scope of the material respectively.

Methodology in Plain English

The author did not run a controlled experiment. Instead, the paper analyzes a live repository over dated observation windows — the archive source census is 21 September 2026 at 06:07 UTC, the public PR records were retrieved 21 September 2026, the last retained review-service report is 13 September 2026, the exposition export is 20 September 2026 at 14:24 UTC, and the LeanEval reuse analysis was retrieved 12 September 2026.

Evidence comes from four sources. First, retained source history and public PR records, which supply contribution attribution, accepted optimization changes, and review outcomes. Second, historical upgrade replays: earlier rows of the migration table re-run the original pre-upgrade source against the new environment to measure breakage, while the final row uses a retained production probe. Third, fresh clean library builds measured on one machine with prebuilt dependencies, compiling inputs preloaded, and artifact restoration disabled, with peak memory sampled as summed proportional resident memory of the build process group. Fourth, retained automated review reports, from which price estimates and verdicts are tallied.

The archive's own automation runs as jobs in a separate repository: discovery jobs scan for completed formalizations under permissive licenses, an open-PR review job inspects submissions and repairs eligible branches, an optimization job profiles existing projects and proposes shortenings, and a dependency-bump workflow probes projects and assigns failures to repair agents. Admission combines the Lean kernel, Mathlib's environment and text-style linters, an archive-specific quality checker, an allowed-axiom audit, project-card validation, and LLM mathematical review of the submission's claims. The author states that reported numbers are computed from retained source and execution records rather than synthetic measurements, that validation checks source hashes and recomputes aggregates, and that the human-written portion of the paper is a single page with the rest produced almost entirely by AI.

Why This Matters

The paper treats maintenance, not generation, as the central problem of AI-assisted mathematics. It argues that a proof is only useful to later work if it still compiles against the libraries that new work depends on, and it supplies an operational record showing what that maintenance actually costs and how often it fails. Its vision is a formal counterpart to arXiv: as formalization becomes easier, new mathematics would arrive with a paper and a maintained formalization, and later work would cite the paper and import the formalization so that formal dependencies mirror the dependency graph of the literature.

Real-world applications:

• Machine-checked review of AI-generated mathematics. The paper points to OpenAI's Ten Advances in Mathematics and Theoretical Computer Science and Finite Time Blowup for Navier–Stokes as examples where large AI-generated arguments were released alongside Lean formalizations, letting correctness be checked mechanically while the ideas are still being absorbed.
• Long-term preservation of research code. Formalizations become foundations for later work; without maintained compatibility they decay as dependency versions move.
• Semantic discovery of formal results. Octo semantic search, the exposition site, and project cards let a reader move from a mathematical question to candidate declarations, inspect their assumptions and definitions, and find import paths.
• Providing provenance for mixed human-AI work. Project cards record upstream authorship and distinguish human-written, AI-written, and mixed proofs even when an agent performs the import.

Industry relevance: The paper contrasts its model with adjacent projects in the Lean ecosystem. Tau Ceti integrates AI-authored mathematics built on human roadmaps into a shared API and makes performance regression a merge condition; Palomar Registry persists verified versions of separate repositories, with updates requiring resubmission, verification, and review; Mathlib relies on human contributors with disclosed AI use and community maintenance across Lean releases. Lean Pool's distinguishing choice is to maintain independent developments together while preserving their attribution and organization. For engineering organizations, the archive is a case study in agent-driven dependency upgrades, advisory versus required performance gates, and the cost of large automated reviews.

Future Directions

• Whether the archive can keep pace as Lean and Mathlib change. The upgrade record shows breakage that never reaches zero automatically — the move to stable Lean 4.34.0 required follow-up integration after initial repair jobs, including updates to supporting APIs.
• The tradeoff between reusable interfaces and compilation cost. The Navier–Stokes refactor added reusable APIs while project build time rose from 879.67 to 887.78 seconds, and library-wide compression reduced lines (45,217) while peak RAM rose from 26.1 to 26.9 GiB. How to balance these is left open.
• How much review is enough, and what it should cost. The paper reports a service redesign and pause, differing billing regimes, and no independently labeled measure of review accuracy, leaving review reliability an open question.
• Whether the arXiv analogy holds. The proposal assumes most new mathematics papers will eventually ship maintained formalizations, which would require the discovery and pooling pipelines to scale well beyond the current 211 projects and 18 contributors.

Target Audience

Researchers and engineers working on formal verification, proof assistants, and AI for mathematics; maintainers of large Lean or Mathlib-dependent codebases; and anyone studying human-AI collaboration in software maintenance. Readers interested in automated review, dependency migration at scale, or the practical economics of AI agents in research infrastructure will find the operational tables most useful, while those seeking new mathematical results should treat the archive itself as the artifact of interest.

Authors’ abstract

Lean Pool is a repository of formalized mathematics. It is grown, maintained and optimized by AI agents.