Vilin97lean-pool0.1.0

#math

Lean Pool logo

lean-pool

Lean Action CI Documentation Exposition 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. See MOTIVATION.md for the why, browse the API docs at https://vilin97.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.

289 formalization projects · 9,933,135 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.

Import PRs can be refreshed automatically after other projects merge. The rebase helper resolves conflicts in the project registry and generated index, preserving module headers and public imports when the index uses them. Conflicts in proof files require a manual rebase.

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}
}