Mathlib

Lean's unified mathematical library, and the reason Lean rather than a rival assistant became the substrate for machine-checked mathematics. The Lean site calls it "over a million lines of formalized mathematics spanning algebra, analysis, topology, probability, and computer science." Community-owned (leanprover-community), Apache-2.0, and read from the GitHub API on 2026-09-06 at 4,041 stars, 1,651 forks, 3,353 open issues, created 2021-05-09 and pushed the same day this page was written.

The fork-to-star ratio is the interesting number and it is inverted from every other repository this corpus holds: 1,651 forks against 4,041 stars, where a normal project runs ten stars to a fork. Mathlib is not a thing people bookmark, it is a thing people commit to. Mathlib4 passed 20,000 contributions in January 2025.

What makes it one library rather than many

Most proof assistants accumulate scattered developments that do not compose, because two authors formalize the same object differently and their theorems will not talk to each other. Mathlib's design decision is a single shared hierarchy of definitions that everything is built against, with a review process that enforces it. That is why the FLT formalization can be measured against Mathlib at all — 13 million lines against a library "5× smaller" is a coherent comparison only because both sit on one set of definitions.

The cost is the well-known one: contributing requires adopting the hierarchy, so the barrier is social and architectural rather than technical, and refactors ripple across the whole library.

It is a library of definitions before it is a library of proofs. Buzzard gives as one of his four reasons for formalizing FLT that many standard objects of modern number theory "have not even been defined in Lean or any other theorem prover," so it is currently not possible to state recent results, let alone prove them. On that reading Mathlib's coverage is the limit on what a machine can be asked about at all, and formalizing a hard theorem is a way of forcing the missing definitions into existence. It also explains why a project can be scooped on its theorem and continue: the definitions were the deliverable.

The 2023 port, and what it proves

The Lean 3 → Lean 4 port completed in July 2023. A community rewrote its entire mathematical library to follow a breaking language change, which is the single strongest piece of evidence in this corpus that Lean's community is load-bearing rather than nominal. Nothing else the wiki tracks has survived that kind of migration intact.

Refreshed 2026-09-06 from Lean's own Mathlib use-case page

lean-lang.org/use-cases/mathlib/ arrived via Telegram minutes after this page was created. It is written for "decision-makers considering Lean and Mathlib for their organizations" — T1 for the library's process and coverage, T3 for the adoption pitch around it.

A first-party contradiction, recorded rather than resolved. Lean's front page says Mathlib is "over a million lines of formalized mathematics." This page, on the same site, read the same day, says "over two million lines" — twice, including in the quality-assurance section. Both are the project describing itself. The corpus keeps the larger figure nowhere: it records that the vendor publishes two numbers a factor of two apart and that neither is dated, which is the honest state.

The review rule that produces the single hierarchy. This page states the mechanism the page above inferred: "A human expert reviews each contribution before it is accepted, and only the strongest approach to any given topic is included. Maintaining the cohesiveness of the library as a whole is a key goal of the review process." That is an editorial monopoly per topic, deliberately chosen — the opposite of a package registry, and the reason formalizations compose. It is also the barrier to entry restated from the maintainers' side.

Quality assurance is tooled, and there is a paper about it. Automated linters over definitions, type-class instances and simp lemmas; CI for compatibility; systematic documentation infrastructure. The page cites Maintaining a Library of Formal Mathematics (van Doorn, Ebner, Lewis, arXiv:2004.03673), which the corpus does not hold and which is the obvious next source for anyone wanting the mechanism rather than the summary.

The Mathlib Initiative has an institutional home. It is a strategic program of Renaissance Philanthropy, established "to ensure the long-term continuity of Mathlib as a high-quality library" and to give its volunteer contributors professional support. That answers half of what lean-fro's page flagged as unresearched, and sharpens the other half: the FRO is time-boxed, the Mathlib Initiative is framed around continuity, and they are separate organizations.

Coverage and who uses it

Stated coverage: abstract algebra, analysis, combinatorics, dynamics, geometry, linear algebra, probability and number theory, plus CS foundations — data structures, logic, computability and complexity theory.

Named research projects: the Polynomial Freiman–Ruzsa conjecture (led by Terence Tao) and the Liquid Tensor Experiment (Commelin and Topaz, with Peter Scholze). Named industrial users: AWS's SampCert for differential privacy in Clean Rooms, multiple tracks of the zkEVM project verifying zero-knowledge circuits and cryptographic protocols, and Starkware's Cairo language, formally verified with heavy Mathlib reliance.

That last group is a live cross-spoke seam. ../cryptography-wiki owns proof systems and the concrete-efficiency frontier; here the same zkEVM and Cairo work shows up as consumers of a mathematical library. Cross-link rather than duplicate — the scheme is theirs, the library is here.

And the AI dependency runs the other way too. DeepMind's alphaproof reached IMO silver by training on Mathlib, and Project Numina is built on it. The corpus has held AlphaProof since May as an application of Lean; the training-data relationship to the library is what this page adds, and it is the concrete form of Buzzard's second reason for formalizing at scale.

Money arrives, 2025

Half of Alex Gerko's July 2025 $10M went to a new Mathlib Initiative (launched September 2025), separate from the FRO itself and run as a program of Renaissance Philanthropy. A volunteer library with its own funded institution is a governance change, not just a budget one. The Initiative's stated job is long-term continuity and professional support for volunteers; how it relates to the community's own review authority is still unread.

The AI seam

Mathlib is what makes autoformalization tractable: a model writing Lean is writing against a million lines of pre-formalized mathematics rather than from nothing, and every benchmark in this area (miniF2F, ProofNet, LeanDojo) assumes it. The FRO chronology records Tau Ceti (July 2026) as "AI-authored Lean mathematics downstream of Mathlib, with human-owned roadmaps and AI adversarial review against open rubrics" — a deliberate architectural choice to keep machine output downstream of the curated library rather than inside it. Whether that boundary holds as AI-generated formalization scales is an open question the corpus should follow.

lean-theorem-prover · lean-fro · lean-lang-org · autoformalization · flt-formalization-anthropic · flt-imperial-project · formal-verification · leonardo-de-moura · alphaproof