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/.
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 LeanPool, install Python toolingSee CONTRIBUTING.md.
Created as part of the UW Lean Hackathon by Vasily Ilin and Justin Asher.