Lean Pool: An AI-Maintained Archive of Formalized Mathematics
cs.AI
Quick verdict
AI-maintained archive of 211 Lean formalizations (3.23M lines) with operational records, but review accuracy and reuse claims lack independent validation.
Summary
Lean Pool is a public repository of 211 completed Lean 4 formalizations (~3.23 million lines, ~194,000 declarations) that is grown, kept compatible with evolving Lean/Mathlib releases, and optimized primarily by AI agents, while the Lean kernel guarantees proof correctness. Admission requires complete proofs (no sorry/admit), a whitelist of three standard axioms, Apache-2.0/MIT licensing, and project cards preserving attribution; quality is policed by linters, an axiom audit, and an LLM mathematical review service. The paper analyzes the archive's operational record: six dependency upgrades repaired up to 100 failing projects per bump (97 in the 4.34.0 stable migration), and accepted optimizations cut library build time by up to 5.8% and removed up to ~55,000 lines, though one golfing change increased build time by 5.4%. Retained review reports (296, mostly approvals; estimated cost $308.52 in the API era plus $752.38 for six Codex-era reviews) and a LeanEval audit citing Lean Pool as the most reused external repository support the review and reuse claims. Main limitations: review accuracy was never independently labeled, the review service was manually disabled before observation, provenance labels do not separate human from agent labor, and the reuse evidence rests on an unpublished manuscript. The paper is largely AI-written, with detailed appendices that allow re-derivation from retained records.
Review complete
Assessment at a glance
5
risk flags identified
● high 0
● medium 2
● low 3
4 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- Lean Pool maintains 211 completed Lean 4 formalizations (~3.23M lines, 193,862 declarations) in a shared environment grown, upgraded, and optimized primarily by AI agents, with proof correctness guaranteed by the Lean kernel.
- Agent-assisted dependency maintenance restored compatibility across six Lean/Mathlib upgrades, repairing up to 100 failing projects per bump (97 in the 4.34.0 stable migration, Table 2/18).
- Accepted optimization changes shortened proofs and improved builds library-wide — up to 5.8% clean-build time reduction and ~55,000 lines removed (Tables 3, 20) — though not uniformly (one golfing change was 5.4% slower).
- A deployed LLM mathematical review service produced 296 retained reports (mostly approvals, Table 5/Fig. 3), and archived mathematics is reused in subsequent research-level formalizations per the LeanEval audit (Fig. 6, Table 24).
- The archive can serve as a maintained formal counterpart to arXiv, preserving attribution while keeping formalizations usable as libraries evolve.
Strengths
Kernel-anchored correctness with candid reporting of negative results
Proofs are machine-checked by the Lean kernel (axiom whitelist, no sorry/admit), and the paper openly reports unfavorable outcomes: PR 246 golfing made clean builds 5.4% slower (Table 3), PR 187 raised peak RAM 26.1→26.9 GiB, the Navier–Stokes API refactor added 8.1 s (Table 4), and the review service was manually disabled before observation (Appendix F).
Unusually detailed and auditable operational record
Table 18 logs the 4.34.0 migration end-to-end (191 probe projects, 97 failures, 95/97 repair jobs succeeded, 639 files, 5,951-line churn); Table 19 gives churn per upgrade; Table 20 reports full before/after build metrics (wall, CPU hours, proportional-set RAM) under a stated protocol; Tables 25–26 list upstream Lean versions and publication concordance for all 211 projects.
Well-specified admission pipeline and CI, benchmarked against peers
Findability and reuse evidence beyond self-report
Weaknesses
Review quality — the load-bearing claim — is unvalidated
Headline reuse claim depends on an unpublished, anonymous audit
Measurement heterogeneity across the optimization tables
Provenance and effort accounting are coarse
Sustainability and objectivity risks of a single-maintainer, AI-written manuscript
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
This is a system/infrastructure paper describing Lean Pool: a repository of 211 completed Lean 4 formalizations (3,228,485 physical lines, 193,862 declarations, 837 registered main results — Table 1) grown, maintained, and optimized primarily by AI agents under a human maintainer. The claim set is threefold: (1) agent-assisted maintenance keeps an independently contributed archive compatible across six Lean/Mathlib upgrades (Table 2); (2) accepted optimizations deliver library-wide proof shortening and compile-time/memory gains (Tables 3–4); (3) an LLM review service plus mechanical checks provide statement-level quality control, and archived mathematics is reused in later research-level formalizations (LeanEval audit, Fig. 6). The 'formal arXiv' vision is explicitly aspirational. The author discloses that the paper is almost entirely AI-written, with a single human-written page.
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 4 strengths & 5 weaknesses, analyzed in detail
- 5 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is Lean Pool?
Lean Pool is a public archive of completed mathematical formalizations in the Lean 4 proof assistant (211 projects, ~3.23 million lines at the time of the paper). It is grown, kept compatible with new Lean/Mathlib versions, and optimized mainly by AI agents, while the Lean kernel mechanically guarantees every proof is correct.
How does Lean Pool differ from Mathlib or the Archive of Formal Proofs?
Mathlib is a single human-reviewed integrated library that grows slowly under strict review; the AFP reviews contributed Isabelle developments. Lean Pool instead pools independently completed projects — human- or AI-written — under lighter admission rules (permissive license, axiom checks, an LLM statement review), preserving each project's attribution and structure.
Are the proofs in Lean Pool trustworthy?
Yes for correctness: entries must contain no sorry/admit, may introduce no axioms beyond the three standard ones, and are checked by the Lean kernel and a compiled-environment audit. Statement faithfulness (does the formal statement match the claimed theorem?) is checked by linters plus an LLM review whose accuracy the paper admits was never independently validated.
How big is Lean Pool and who maintains it?
At observation it held 211 completed projects, 7,043 Lean files, 3,228,485 lines, 193,862 declarations, and 837 registered main results, with 18 human contributors; daily agent jobs handle discovery, review support, optimization, announcements, and dependency upgrades.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Text extraction omitted parts of the middle (Table 8, part of the §9 positioning discussion, Table 10 capture dates, and Appendix A observation windows), so some secondary details could not be checked directly.
- Figures 1-6 are available only via captions and surrounding text; visual content (e.g., Figure 2 growth curves) was not analyzable.
- References are partially truncated in extraction; citation completeness beyond the visible entries was not verified.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.