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/.
117 formalization projects · 841,688 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.
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 toolingTo work on a single project you don't need the whole pool built — see the
fast per-project build in CONTRIBUTING.md.
See CONTRIBUTING.md.
Created as part of the UW Lean Hackathon by Vasily Ilin and Justin Asher.