Lean Pool: An AI-Maintained Archive of Formalized Mathematics
Vasily Ilin
cs.AI
2026-09-22
Lean Pool is an AI-maintained archive of finished Lean formalizations: 211 projects, 3.23M lines. One library-wide compression dropped 45,217 lines and cut a clean build by 3.3%.
Lean can check a proof mechanically. Mathlib still grows at a roughly linear rate because humans review every merge, and much of research-level mathematics is missing from it. Long arguments that ship with Lean formalizations already treat a checked proof as a companion to the paper. A companion that later work cannot import is a dead artifact. Isolated repositories break as soon as Lean or Mathlib moves.
Vasily Ilin at the University of Washington built Lean Pool: finished formalizations of named, known results, kept in one Lean and Mathlib environment. AI agents discover, upgrade, and compress; humans watch the merges. The stated aim is a low-friction formal counterpart to arXiv.
Work enters on two paths. Agents hunt complete Apache-2.0 or MIT formalization projects, bump the Lean version, pass CI and linters plus an LLM reviewer, then trim compile time and RAM. Humans also submit their own projects. Only serious, finished formalizations of named results qualify. Human, AI, and mixed authorship are all eligible.
Admission is strict: no sorry or admit; axioms limited to Classical.choice, propext, and Quot.sound; no setoption and no tricks that bypass resource limits; every project carries a card with authors, upstream source, proof provenance, and informal statements of the main results.
Daily jobs search for projects, inspect open PRs, work maintainer issues, golf existing code, and announce accepts on Zulip. A dependency-update workflow probes new Lean and Mathlib releases, assigns failing projects to repair agents, and bundles the patches for review. A mathematical review service checks faithfulness, duplication, and code quality. Maintainers can revise from the report.
At the observation snapshot: 211 completed projects, 7,043 Lean files, 3,228,485 physical source lines, 193,862 declaration commands, 837 registered main results. Provenance is 70 human / 102 AI / 39 mixed. Eighteen GitHub accounts have commits; 63 community PRs merged. The Lean version has been bumped six times.
The largest single project is the finite-time Navier–Stokes and Euler blowup development, AI-authored, 641,073 lines. The Gödel incompleteness development is human-authored, 55,430 lines.
Upgrades hurt. Moving 4.32.0-rc1 to 4.33.0-rc1 broke 100 of 143 projects at the compiler. Moving 4.34.0-rc1 to stable 4.34.0 broke 97 of 191. Some hops are cheap: 4.33.0-rc2 to 4.34.0-rc1 failed only 3 of 148. The stable migration launched 97 repair jobs, 95 succeeded, and the remaining two (graph fundamental group, incompleteness) needed follow-up integration: 639 files, 5,951 lines of churn.
Library-wide compression removed 45,217 lines and cut a clean build from 16.11 to 15.59 minutes (3.3% faster). An elaboration-cost pass removed 54,965 lines and went 28.46 to 26.82 minutes (5.8% faster). Contributor golfing removed 12,515 lines and made the build 5.4% slower, with a small RAM drop. Extracting reusable Navier–Stokes APIs moved one project from 879.67 to 887.78 seconds.
On one Azure VM, Lean Pool takes 60.28 minutes and 20.03 GiB peak RAM for a clean build; Mathlib at the matching release takes 37.44 minutes and 7.35 GiB. In the LeanEval structural audit, Lean Pool is the most reused external repository by matching declarations.
The LLM reviewer left 188 approvals, 71 change requests, and 37 discussion verdicts. Historical API price estimates on 285 reports total $308.52 (median $0.20). Six later Codex-equivalent estimates total $752.38 (median $89.03). On 69 same-PR review pairs, only 37 share a verdict. The structured review service was manually disabled before the observation date.
Autoformalization is producing artifacts faster than Mathlib can absorb them. Lean Pool does not fold projects into one shared API, which is the Mathlib and Tau Ceti model. It keeps independent developments compiling together, searchable, and importable. For proving agents that is closer to how the work actually ships: a project stays a project, and citations are a separate graph.
Practitioners can depend on it today. People who train formalization agents get an operations log with CI, upgrade failure rates, and accepted optimizations, not a design sketch.
The author states that the human-written portion is a single page and the rest is produced almost entirely by AI. Reported numbers are computed from retained source and execution records with hash checks, so the measurements are not synthetic. The prose still has to be read as AI-drafted, human-owned.
LLM review accuracy was never independently labeled; the census records merge and close decisions. Repeated reviews of the same PR agree on 37 of 69 pairs. The service is off, so recent imports are outside that coverage. Agent repairs still needed follow-up integration, and the stable migration changed auxiliary hypotheses around measurability and sigma-finiteness. A green build does not mean every declaration type is equivalent across the upgrade. Golfing can slow compiles. Reusable interfaces carry a compile tax. The archive is heavier and more RAM-hungry than Mathlib; whether agents keep up past Lean 4.34 is an open operations question, not a result in this paper.