Lean Pool
Lean Pool keeps Lean projects that are outside Mathlib's scope. As its README describes, each is imported from a permissively licensed repository into a directory of its own, brought to Lean Pool's Lean and Mathlib, and merged once it passes Lean Pool's CI and an LLM review. This chapter maps its 334 projects at commit 2b205bf9 (2026-11-08), built with Lean v4.35.0 and Mathlib at 56a00585. Each project has a card, LeanPool/projects/<slug>.yaml, with its title, summary, authors, sources, license, provenance, MSC2020 classes and main results, each a Lean declaration with an informal statement. There is a section per top-level MSC2020 class, the class of the first code a card lists (40 sections), and an article per card, titled by the card's title. An article quotes the card's summary, names its authors, links its sources and the project's own repository, gives its provenance and license, and lists its main results.
The cards list 1,341 main results, 509 of them among the cards' main declarations, whose names Lean Pool's CI checks with #check. No Lean is run for this chapter: each main result's declaration is looked for in its project's files by reading the source text, following namespace, section and end, and a name counts only when a declaration command names it in full under the namespaces it sits in, in one file of the project. The scan finds 1,331 of the 1,341 declarations, and 508 of the 509 main declarations. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at the pinned commit; a main result the scan does not find keeps its informal statement and says so. Articles show no Lean signatures and have no dependencies, as edges between declarations need Lean.
A card's provenance says who wrote the project's Lean proofs, in the words of Lean Pool's contributing guide: “human” (“written by people”), “AI” (“mostly produced by an AI system”) or “mix” (“both contributed substantially”). Of the cards, 207 say AI, 73 human and 54 mix.
The quoted text is the cards', in Lean Pool's repository under the Apache-2.0 license, as written, except that a < before a letter, or an & that would start a character reference, which the site cannot show as text, is set in code. Each article names the project's authors and shows these fields of its card's source, where the card has them: the DOI, arXiv id and URL, and a paper, manuscript, proof or problem page, each linked; the citation; the mathematical source, background and notes, quoted; and the project's repository and commit. A card may hold other source fields, which are not shown. Of the projects, 48 were published under the MIT license, and Lean Pool redistributes them under Apache-2.0; where Lean Pool's notice file keeps a copyright line or a note for one, its article quotes it.
MSC2020 classes 03 to 35
- Mathematical logic and foundations
- Combinatorics
- Order, lattices, ordered algebraic structures
- Number theory
- Field theory and polynomials
- Commutative algebra
- Algebraic geometry
- Linear and multilinear algebra; matrix theory
- Associative rings and algebras
- Nonassociative rings and algebras
- Category theory; homological algebra
- Group theory and generalizations
- Topological groups, Lie groups
- Real functions
- Measure and integration
- Functions of a complex variable
- Several complex variables and analytic spaces
- Special functions
- Ordinary differential equations
- Partial differential equations
MSC2020 classes 37 to 94
- Dynamical systems and ergodic theory
- Harmonic analysis on Euclidean spaces
- Functional analysis
- Operator theory
- Calculus of variations and optimal control; optimization
- Geometry
- Convex and discrete geometry
- Differential geometry
- Algebraic topology
- Manifolds and cell complexes
- Global analysis, analysis on manifolds
- Probability theory and stochastic processes
- Statistics
- Numerical analysis
- Computer science
- Mechanics of particles and systems
- Quantum theory
- Operations research, mathematical programming
- Game theory, economics, finance, and other social and behavioral sciences
- Information and communication theory, circuits
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.