This public fork records my Lean formalization contributions to Lean Pool. It is not a separate curated library: the upstream repository is the authority for accepted contributions, review decisions, and integration checks. Code under discussion lives on the corresponding contribution branches; an open PR is not yet part of upstream main.
These contributions grew out of my work on clique partitions and Erdős problem #81. The papers and their release evidence are maintained separately in erdos-81-chordal-clique-partitions. The contributed Lean code is licensed under Apache-2.0; paper licenses are separate. Proof provenance and the precise scope of each result are recorded in the PRs and project cards. Formalizing a classical theorem is not a claim of new mathematics.
These formalizations accompany my preprint series on Erdős Problem #81
(erdos-81-chordal-clique-partitions),
which I am preparing to submit to arXiv (math.CO). If you are an arXiv author eligible to endorse
in math.CO and found this work valuable, you can endorse me at https://arxiv.org/auth/endorse?x=N8V4R6 (code N8V4R6). An
endorsement only confirms that the work is appropriate for the subject area; it is not a review of
the results. Thank you.
En español: estas formalizaciones acompañan mi serie de preprints sobre el problema #81 de Erdős,
que preparo para enviar a arXiv (math.CO). Si eres autor de arXiv habilitado para dar endorsement
en math.CO y este trabajo te pareció valioso, puedes dármelo en https://arxiv.org/auth/endorse?x=N8V4R6 (código N8V4R6). El
endorsement solo confirma que el trabajo es adecuado para el área; no es una revisión de los
resultados. ¡Gracias!
| Contribution | Upstream PR |
|---|---|
| Finite cone and linear-programming duality | #347 |
| Sum-zero triangle packing | #348 |
| Chordal separators and Dirac theorems | #349 |
| Minimum-degree and spread matching theorems | #420 |
| Bennett–Bernstein, Freedman, and Hoeffding inequalities | #431 |
| Finite max-flow/min-cut | #432 |
| Even graph cycle decomposition | #433 |
| Finite near-regular hypergraph nibble | #471 |
| Asymptotic triangle-packing gap | #544 |
| Dross's fractional triangle decomposition theorem | #573 |
| Clique-tree theory for chordal graphs | #577 |
| Vizing's theorem and equitable edge colourings | #578 |
| Clique-forest/tree-decomposition and colouring/matching adapters | #579 |
| Retained-clique gluing and exact induced-piece accounting | #580 |
| Strict Beck–Fiala matrix rounding | #581 |
| Brooks' theorem for finite subcubic graphs | #582 |
| Gavril subtree representations and exact chordal treewidth | #583 |
| Häggkvist–Janssen complete-graph list edge colouring | #585 |
| Structural graph classes: split partitions, cotrees and threshold creation sequences | #587 |
All 19 contributions above are merged upstream; there are no open contribution PRs.
Status snapshot: 17 October 2026 (America/Santiago). The upstream repository is now LeanPool/lean-pool; the linked PRs show live status. The earlier #464 repair proposal was closed without merge and is not counted as an accepted contribution.
The original Lean Pool README follows, preserving its attribution and documentation. Its generated statistics describe the upstream project, not my contribution totals.
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.
203 formalization projects · 2,910,436 lines of Lean · 2 open challenges
(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 the Azure VM's Codex account pool, 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.
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.
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.