Lean Pool: An AI-Maintained Archive of Formalized Mathematics

It proposes and operates a "living" archive of formalized mathematics that pools independently developed, variously sourced completed projects into a common Lean/Mathlib environment while preserving attribution and project organization. Unlike an integrated library such as Mathlib, which grows linearly under strict human review, Lean Pool admits human, AI, and mixed projects through pooling plus agent maintenance; admission requires no sorry or admit, no axioms beyond Classical.choice, propext, and Quot.sound, an Apache-2.0 or MIT license, and a project card identifying authors, upstream source, proof provenance, and main results. The paper reports an archive census: 211 completed projects, 7,043 Lean source files, 3,228,485 physical source lines, 193,862 source declaration commands, 837 registered main results, human/AI/mixed projects of 70/102/39, 18 commit contributors, 17 contributors with merged PRs, and 63 merged community PRs.

Agent-assisted dependency upgrades can restore compatibility of the archive after Lean/Mathlib version changes. The paper moves the reusability of formalizations beyond preserving source: a dependency-update workflow detects new releases, builds the archive, assigns failing projects to repair agents, and checks the repaired projects together. Table 2 records projects at probe and compiler failures across six historical upgrades, for example 59 projects at probe and 44 compiler failures from 4.30.0-rc2 to 4.31.0-rc1, and 191 projects and 97 failures from 4.34.0-rc1 to 4.34.0. Appendix D records the stable-version migration: 191 probe projects, 97 compiler failures, 95 of 97 repair jobs succeeded and 2 failed, with 198 accepted projects, 639 changed files, and 5,951 lines of churn.

A shared archive enables cross-project proof shortening and compilation optimization, with measurable build-resource changes. The paper reports not only shorter proofs but before/after whole-library build time and peak memory, plus project-level compilation seconds. Table 3 lists accepted changes, for example change 187 "Library-wide compression" removed 45,217 lines with build time moving from 16.11 to 15.59 minutes and peak RAM from 26.1 to 26.9 GiB, and change 339 "Elaboration-cost reduction" removed 54,965 lines with build time moving from 28.46 to 26.82 minutes. Table 4 gives project-level results, for example quantum parallel repetition moving from 141.85 to 86.08 seconds. Appendix A.2 reports clean-build comparisons: Lean Pool at 3.23 MLOC, 60.28 minutes, 20.03 GiB, versus Mathlib (matching release) at 2.33 MLOC, 37.44 minutes, 7.35 GiB.

It brings "whether a statement is faithful to the advertised mathematical contribution" into admission, alongside a searchable exposition site and dependency graphs. The Lean kernel only guarantees that a proof is correct; the paper adds a mathematical review service examining faithfulness, novelty, significance, sources, and code quality, and an exposition site linking project cards, informal accounts, Lean statements, and dependency graphs. The review service recorded 285 historical API-estimate reports totaling $308.52 with a median of $0.20; among 69 repeated-review pairs on the same PR, 37 gave the same verdict. Exposition coverage includes 203 documented projects, 173,362 source declarations, 124,412 theorems and lemmas, 1,389,967 dependency links, and 87,408 declarations used by multiple others. Appendix G.1 records reuse of archived results by later developments such as Kurosh, Feige, and Poincaré.

The work targets completed formalizations of named known results, requiring no sorry or admit, restricted axioms, an Apache-2.0 or MIT license, and a project card identifying authors, upstream source, proof provenance, and main results; open challenges are kept separately on a challenge board and are not part of the completed set. It lets human contributors, AI agents, and later researchers submit, find, inspect, and reuse formalizations within a common Lean/Mathlib environment, and makes dependency upgrades and optimization repeatable daily processes. The paper positions Lean Pool as a living archive of formalized mathematics whose aim is to keep formalizations usable as Lean and Mathlib evolve, rather than to replace the informal mathematical literature itself.

The paper states that the archive and its automation repository keep changing and that observations have explicit timestamps (for example, the source census is September 21, 2026, 06:07 UTC), so the reported numbers are snapshots at particular revisions. The review service was manually disabled before the current observation, so retained reports describe past executions and do not establish ongoing coverage of the most recent imports; prices are estimates attached to retained reports rather than invoices, and overwritten or unrecorded executions are not recoverable from retained comments. Appendix D notes that a successful build establishes compatibility of the accepted statements but does not establish equivalence of every declaration type before and after the upgrade. In addition, the human-written portion of the paper is a single page and the rest is produced almost entirely by AI, so readers wanting finer proof details should consult the appendices, source revisions, and public PR records.