Skip to content

README.md

Latest commit

 

History

History
92 lines (67 loc) · 5.63 KB

README.md

File metadata and controls

92 lines (67 loc) · 5.63 KB
Raw

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.

312 formalization projects · 11,745,320 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.

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.

Contributing

See CONTRIBUTING.md.

Every PR, including drafts, gets an advisory compile-cost comment, refreshed after pushes. PRs without added or modified Lean files get a no-files report. The PR author or a maintainer can also comment /profile to rerun it. 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}
}