lean-pool

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, and browse the API docs at https://vilin97.github.io/lean-pool/.

129 formalization projects · 900,009 lines of Lean

_{(stats above are refreshed automatically by readme-stats.yml — 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.

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.