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.
141 formalization projects · 946,790 lines of Lean · 2 open challenges
(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.
Challenge/ is the other half of the pool: open statements rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as sorry, registered in Challenge/challenges.yml alongside the English statement it is supposed to say. It is the only place sorry is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies.
Anyone can propose one. The LLM reviewer judges a challenge on different grounds than a project: whether the problem is significant, whether the Lean faithfully says what the prose says, whether a cited known result is stated the way its source states it, whether the statement is vacuous or gameable, and how many lines of Lean a solution would take.
Anyone can answer one, too. A solution lands in Solution/, restating the statement and proving it, and leanprover/comparator settles whether it counts: CI exports the challenge and solution environments separately, checks that the statements agree, and replays the proof through the Lean kernel with no axiom beyond propext/Quot.sound/Classical.choice. Because a kernel decides correctness, the solution review is short — and is skipped entirely when the PR adds nothing but the answer.
make challenges # what's on the board
make verify-challenge C=<slug> # replay a solution locallySee Challenge mode in CONTRIBUTING.md.
See CONTRIBUTING.md.
Created as part of the UW Lean Hackathon by Vasily Ilin and Justin Asher.
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.