LeanPoollean-pool0.1.0

#math

Lean Pool logo

lean-pool

Lean Action CI Documentation Exposition Source profile Zulip Semantic Search License DOI arXiv

Lean Pool sits between mathlib and merely-true, preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying sorry-free and pinned to the latest Mathlib. Tau Ceti is also a pinned Lake dependency; import its modules directly instead of vendoring projects already in Tau Ceti or Mathlib. See MOTIVATION.md for the why, browse the API docs at https://leanpool.github.io/lean-pool/, and explore each project's dependency graph and declarations in the exposition site.

Semantic search is also available via the API.

Explore compile costs in the LeanPool source profile, from projects and files down to declarations and source lines. The weekly profiling job runs on our Azure VM; the badge shows the date of the latest completed recording.

298 formalization projects · 10,977,403 lines of Lean

(stats above are refreshed automatically by the generated-metadata workflow — edit python/lean_pool/stats.py, not the numbers)

So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass CI — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no sorry/admit, no axioms beyond Classical.choice/propext/Quot.sound, no unsafe/partial, file headers, size limits) — and an LLM review of fit and significance, then merged.

LLM reviews use GPT-6-Astra at xhigh reasoning effort through a privately operated Codex worker, without paid OpenAI API requests or an API fallback. Reviews also show an estimated dollar cost at official Standard API token rates, labeled separately from Codex quota billing. See review operations for deployment and diagnostics.

Project PRs also receive an advisory Greptile review, configured in .greptile/, for cross-file integration, reusable abstractions, completeness, maintainability, and measured cost. It supplements rather than replaces the independent LLM verdict.

Getting started

Requires Lean (via elan, with the toolchain pinned in lean-toolchain) and Python 3.13+ with uv.

make setup    # pull Mathlib oleans, build the whole pool (~1.5h), install Python tooling

To work on a single project you don't need the whole pool built — see the fast per-project build in CONTRIBUTING.md.

To regenerate the preserved Zeta5 numerical certificates, see the certificate reproduction guide.

The moving-sofa certificate recipe regenerates its optimized certificate modules from pinned public inputs.

Contributing

See CONTRIBUTING.md.

The PR author or a maintainer can comment /profile to request an advisory compile-cost report. Failed or zero-phase timed runs show unavailable timing and are excluded from totals; errors and any successfully measured heartbeat counts remain visible.

Accepted PRs enter GitHub’s merge queue. CI checks the combined changes against current main without repeatedly updating authors’ branches. Each project owns its YAML card and public Imports.lean; there is no shared import list to edit. Conflicts in the same proof files still require a manual repair.

Credits

Created as part of the UW Lean Hackathon by Vasily Ilin and Justin Asher.

Difference from similar projects

Tau Ceti is another approach to solve the same problem. The differences are:

  • Lean Pool accepts human-written projects, not just AI projects.
  • Lean Pool is not a unified library like mathlib. Most projects are independent of each other.
  • Lean Pool only accepts completed formalization projects.

Palomar Registry is also similar to Lean Pool. The differences are:

  • Lean Pool maintains accepted projects.
  • Lean Pool provides tools like search and documentation.
  • Palomar is a registry, not a unified repository.

Projects accepted to the Palomar Registry may be submitted to Lean Pool, and priority will be given to them.

Citation

To cite Lean Pool, use the paper:

@misc{ilin2026leanpool,
  title = {{Lean Pool}: An {AI}-Maintained Archive of Formalized Mathematics},
  author = {Vasily Ilin},
  year = {2026},
  eprint = {2609.25199},
  archivePrefix = {arXiv},
  primaryClass = {cs.AI},
  doi = {10.48550/arXiv.2609.25199},
  url = {https://arxiv.org/abs/2609.25199}
}