Mathlib
Last reviewed
May 18, 2026
Sources
No citations yet
Review status
Needs citations
Revision
v1 · 3,951 words
Improve this article
Add missing citations, update stale details, or suggest a clearer explanation.
Suggest edit
CtrlK
Last reviewed
May 18, 2026
Sources
No citations yet
Review status
Needs citations
Revision
v1 · 3,951 words
Add missing citations, update stale details, or suggest a clearer explanation.
Mathlib (formally mathlib4, the active Lean 4 incarnation) is a community-maintained, open-source library of formalized mathematics written in the lean theorem prover. Begun in 2017 as a separate repository for math-focused additions to Lean's then-nascent ecosystem, Mathlib has grown into the largest unified formalization of mathematics in any proof assistant.[^1][^2] As of May 2025, the library contained roughly 210,000 theorems, 100,000 definitions, and the contributions of over 500 named authors across more than 2 million lines of Lean code, with the project's own statistics page showing 274,045 theorems, 130,791 definitions, and 772 contributors by 2026.[^3][^4][^5]
Mathlib occupies an unusual position in the contemporary mathematical and artificial-intelligence ecosystems. To working mathematicians, it is the practical embodiment of the formalization movement, a single library that already contains undergraduate analysis, abstract algebra, topology, measure theory, category theory, much of algebraic geometry, and substantial fragments of frontier research mathematics such as condensed-vector-space theory and the Polynomial Freiman-Ruzsa conjecture.[^6][^7] To machine-learning researchers, Mathlib serves a different but equally critical role: it is the de facto target language and training corpus for AI systems that generate mathematical proofs, including Google DeepMind's alphaproof, DeepSeek-Prover, Goedel-Prover, and many academic systems benchmarked on miniF2F.[^8][^9][^10]
Crucially, Mathlib should be distinguished from Lean itself. Lean is a programming language and proof assistant developed originally by Leonardo de Moura at Microsoft Research and now by the Lean Focused Research Organization. Mathlib is one library that runs on top of Lean. The relationship is roughly analogous to Python and NumPy, or LaTeX and the AMS macros: the underlying engine has its own development team and release cycle, while Mathlib is a separate community project whose contents are mathematics rather than language infrastructure.[^11]
Lean was first released in 2013 as an internal Microsoft Research project; Lean 2 in 2015 and Lean 3 in early 2017 followed. The Lean 3 release coincided with a sharp uptick in interest from research mathematicians, who began submitting math-specific definitions, lemmas, and tactics to the Lean core repository. According to participants, Leonardo de Moura found his time as Lean's principal author increasingly consumed by mathematics-related issues that were peripheral to the language itself, and he suggested that the mathematical content be split off into its own repository.[^12] In 2017 this repository was created under the leanprover-community GitHub organization and given the name mathlib.
Early stewardship was led by Mario Carneiro, a CMU postdoctoral researcher in pure and applied logic, and Johannes Hölzl, also at CMU; both had backgrounds in proof-assistant work (Carneiro had previously formalized mathematics in Metamath). The library grew from roughly 15,000 lines of code to about 140,000 over its first two years.[^13][^12]
The first Mathlib paper, "The Lean mathematical library" (arXiv:1910.09336), was presented at CPP 2020 and characterized the project's distinguishing features: a dependently typed foundation, a deliberate emphasis on classical (rather than constructive) mathematics, an extensive typeclass hierarchy, large- and small-scale tactic automation, and a distributed governance model with no single owner.[^1] A companion paper, "Maintaining a Library of Formal Mathematics" (arXiv:2004.03673), described the tooling for review, linters, and continuous integration that distinguished Mathlib from earlier ad-hoc formalizations.[^14]
In 2021, the Lean development team released Lean 4, a complete rewrite that altered the syntax, metaprogramming model, and elaboration algorithm. Lean 4 was explicitly not backwards compatible with Lean 3.[^11] Because Mathlib had by this point accumulated more than a million lines of code expressing significant mathematical infrastructure, the question of porting was non-trivial.
The community's response had three components. A semi-automated translation tool named mathport converted Lean 3 syntax to Lean 4 syntax on a file-by-file basis, producing scaffolding humans would then refine.[^15] Porting was tracked on a public dashboard listing each module's translation status. Tactics, however, had to be rewritten by hand because of deep differences between Lean 3 and Lean 4 metaprogramming.[^15]
On July 16, 2023, the community declared the port complete. The Lean 3 repository was archived and made read-only, and mathlib4 became the active library.[^16] The tagged release mathlib4:v3-eol marked the last version that still accepted #align statements bridging Lean 3 and Lean 4 names.[^17] In practice this means that since mid-2023, Mathlib refers to mathlib4, and references to "mathlib3" in current literature are historical.
Under Lean 4, Mathlib continued to grow approximately linearly. By late 2025 the library exceeded 2 million lines of code across roughly 8,000 files, with monthly contribution rates reaching new highs.[^4] August 2025 was reported as the library's busiest month to date, with over 1,100 pull requests reviewed and merged; the review queue at any given time has tended to hold several hundred outstanding PRs with median wait times of about two weeks.[^4]
In 2025 the Mathlib Initiative was established as a program of Renaissance Philanthropy with a founding donation from Alex Gerko, founder and CEO of XTX Markets. The Initiative's stated mission is to provide professional editorial, infrastructure, and devops support to the otherwise volunteer-run library, addressing scaling limitations created by the gap between submission volume and reviewer availability. Additional funding has included a $5 million Gerko donation specifically earmarked for Mathlib growth, support from the Alfred P. Sloan Foundation for computational infrastructure, and, beginning in September 2025, the broader AI for Math Fund which announced $18 million in initial grants and a further $13.5 million commitment in early 2026.[^18][^19]
Mathlib is organized as a tree of Lean modules rooted at the Mathlib/ directory. Subdirectories correspond closely to traditional mathematical subjects, and each subdirectory typically contains a sequence of files in dependency order (basic definitions first, more advanced results later). Major top-level subdirectories include:[^20][^6]
Mathlib/Algebra/ for group, ring, field, module, polynomial, and category-theoretic algebra.Mathlib/Analysis/ for normed spaces, Banach and Hilbert spaces, differentiation, special functions, and convexity.Mathlib/Topology/ for general, metric, uniform, and algebraic topology.Mathlib/MeasureTheory/ for measure, integration, and probability.Mathlib/NumberTheory/ for arithmetic, p-adic numbers, modular forms, and L-functions.Mathlib/Geometry/ for affine geometry, manifolds, and Lie groups.Mathlib/CategoryTheory/ for general category theory, including limits, adjoints, and abelian categories.Mathlib/Combinatorics/ for graph theory, additive combinatorics, and enumeration.Mathlib/Logic/, Mathlib/Data/, Mathlib/Order/ and others for foundational infrastructure.In addition to Mathlib/, the repository contains an Archive/ folder of completed but stand-alone formalizations not intended for general import, a Counterexamples/ folder, and a MathlibTest/ test harness.[^2]
A distinguishing technical feature of Mathlib is its extensive algebraic typeclass hierarchy. Mathematical structures such as semigroups, monoids, groups, rings, fields, modules, and topological groups are represented as Lean typeclasses. The hierarchy is pruned to a directed acyclic graph; each node bundles its operators with its axioms, and edges correspond to typeclass instances that automatically derive weaker structures from stronger ones.[^21]
Mathlib's design philosophy is to introduce a new typeclass only when there is "real mathematics to be done with it, or when there is a meaningful gain in simplicity by factoring out a common substructure."[^22] This contrasts with both unbundled approaches (every algebraic property as a separate hypothesis) and naive bundled approaches that suffer exponential blowup through repeated superclass instance parameters. Multiple inheritance is heavily used, so the ordered algebraic hierarchies combine partial-order, lattice, and group hierarchies into combined structures like linearly ordered fields and topological fields.[^21][^22]
Mathlib has detailed naming conventions designed to make identifiers searchable. Lemma names are formed from snake_case words describing the conclusion, with namespaces matching the relevant definition (for example, Nat.add_comm rather than a free-standing nat_add_comm).[^23] Conventions cover formatting, documentation strings, and the structure of induction principles. New contributors are expected to follow these conventions, and continuous-integration linters check many of them automatically.
Mathlib uses a fork-and-pull-request workflow on GitHub.[^24][^25] A contributor forks the repository, creates a branch, opens a pull request against master, and engages in iterative review until approval and merge. Distinctive features include:
maintainer merge to summon final approval.Maintainers have final merge authority. Most reviewers and maintainers are unpaid volunteers, and the resulting bottleneck (several hundred PRs in queue, median waits measured in weeks) is one of the principal motivations for the Mathlib Initiative's professional-support program.[^4]
Among the first projects to demonstrate that Lean and Mathlib could reach research-level mathematics was the perfectoid spaces formalization by Kevin Buzzard, Johan Commelin, and Patrick Massot, completed and reported in the paper "Formalising perfectoid spaces" (arXiv:1910.12320). Perfectoid spaces, introduced by Peter Scholze in 2012, are sophisticated objects in arithmetic geometry that depend on long chains of algebraic and topological prerequisites. The formalization did not prove a new theorem; rather, it formalized enough of the underlying topology, algebra, and geometry to state the definition of a perfectoid space in Lean.[^27]
The project had a substantial side-effect: it exposed scaling issues in Lean 3's typeclass-inference algorithm that motivated significant redesigns in Lean 4. The perfectoid project is often cited as an early proof of concept that Lean's mathematical infrastructure was on a trajectory to handle frontier research.[^27]
In December 2020, Fields medalist Peter Scholze publicly challenged the proof-assistant community to formally verify the central theorem of his joint work with Dustin Clausen on liquid vector spaces, a structural theorem in their then-new theory of condensed mathematics. Scholze posted the challenge on Kevin Buzzard's Xena Project blog, noting that he was personally uncertain whether the proof was correct and would consider formal verification meaningful evidence.[^28][^29]
Led by Johan Commelin with mathematical guidance from Scholze and major contributions from Adam Topaz, Reid Barton, Buzzard, and roughly fifteen others, the Liquid Tensor Experiment (LTE) completed on July 14, 2022, approximately 18 months after the challenge was posed.[^28] The formalized statement was that Ext^i(M_{p'}(S), V) = 0 for all i \geq 1 under appropriate hypotheses on profinite sets S and p-Banach spaces V. Along the way, the formalizers discovered that a key intermediate step (the Breen-Deligne resolution) was not strictly necessary, allowing them and Scholze to formulate a streamlined version of the theorem before the formal proof was finished. The completion was covered in Nature and Quanta Magazine and is widely regarded as a watershed moment for the formalization of contemporary research mathematics.[^28]
The sphere eversion project, led by Floris van Doorn, Patrick Massot, and Oliver Nash, formalized in Lean 3 and Mathlib the existence of a sphere eversion in three-dimensional space, deriving it from a formalization of the h-principle for open and ample first-order differential relations. The project was notable both for the depth of the underlying differential topology (which had not previously been formalized in any proof assistant) and for demonstrating Mathlib's reach into nontrivial geometric topology.[^30]
A formalization by Sander Dahmen, Johannes Hölzl, and Robert Y. Lewis of the Ellenberg-Gijswijt solution to the cap set problem (arXiv:1907.01449) provided an early demonstration that Mathlib's linear-algebra and combinatorics infrastructure was strong enough to support a recent Annals-of-Mathematics-level result. Many of the underlying generic constructions were upstreamed into Mathlib in the process.[^31]
In 2024, Kevin Buzzard, supported by EPSRC grant EP/Y022904/1, launched a five-year project at Imperial College London to formalize the proof of Fermat's Last Theorem in Lean and Mathlib. The strategy, designed in collaboration with Richard Taylor, is not to translate Andrew Wiles's original argument verbatim but to use a modern reformulation incorporating subsequent work by Khare, Wintenberger, Kisin, and others, then to reduce FLT to a set of mathematical claims that were already understood by the late 1980s. The project intends to upstream supporting infrastructure into Mathlib continuously, expanding the library's coverage of arithmetic geometry, modular forms, and Galois representations. The grant runs until September 2029.[^32]
Shortly after the Polynomial Freiman-Ruzsa (PFR) conjecture was settled in 2023 by Timothy Gowers, Ben Green, Freddie Manners, and Terence Tao, Tao launched a public Lean 4 formalization with Yael Dillies and Bhavik Mehta. The project, hosted at github.com/teorth/pfr, formalized a significant portion of the paper within its first three weeks and was completed afterwards, demonstrating that Mathlib was mature enough to absorb fresh research mathematics in a timeframe of weeks rather than years. The project also showcased Patrick Massot's Blueprint tool, which links human-readable LaTeX exposition to the corresponding Lean lemmas.[^33]
Mathlib has become the central artifact for an entire subfield of artificial intelligence research, and its dual function as a verifier and as training data is what distinguishes it from any other resource in formal mathematics.
Most major AI proof systems of the mid-2020s target Lean 4 with Mathlib because Lean's kernel offers reliable proof checking and Mathlib provides the vocabulary of definitions and lemmas needed to even state realistic mathematics. Google DeepMind's alphaproof, which earned a silver-medal-equivalent performance at the 2024 International Mathematical Olympiad, was trained against Lean and used Mathlib's formalized mathematics extensively.[^8][^34] DeepSeek-Prover and DeepSeek-Prover-V2 (the latter built on a 671-billion-parameter base in 2025) are likewise designed for formal theorem proving in Lean 4 against Mathlib's definitions.[^9][^35] goedel prover, an open-source frontier model documented in arXiv:2502.07640, similarly targets Lean 4 and incorporates Mathlib into its training corpus from its sixth training iteration onward.[^10]
The size and uniformity of Mathlib also make it valuable as a corpus for pretraining and fine-tuning language models on mathematical content. By 2025, researchers had used state-transition exploration over Mathlib4 to generate datasets exceeding 4.7 million synthetic theorems totaling roughly 1 billion tokens for use in theorem-proving model training.[^36] Smaller curated datasets aligned to Mathlib, such as numinamath and Herald, provide natural-language-to-Lean translation pairs designed to bootstrap autoformalization and proof generation.
The widely used miniF2F benchmark (488 olympiad-level problems formalized in multiple proof assistants, including Lean) provides a standard evaluation set for theorem-proving models; the Lean version is written against Mathlib and is the most actively used variant.[^37] PutnamBench and other benchmarks similarly rely on Mathlib's vocabulary. The November 2025 reassessment miniF2F-v2 restored several simplifications that had been made in the original benchmark, reducing scores for most theorem provers and showing that benchmark integrity itself depends on careful versioning against Mathlib changes.[^37]
Google DeepMind, through its formal-conjectures and formal-imo repositories on GitHub, has been formalizing open conjectures and competition problems in Lean and depositing them in Mathlib-compatible form, in some cases in collaboration with the Mathlib Initiative on projects such as the Stacks Project.[^19][^38] These collaborations represent an emerging pattern in which industrial AI research and the open-source formal-mathematics community share infrastructure.
A central figure in Mathlib's expansion is Kevin Buzzard, professor of pure mathematics at Imperial College London and specialist in arithmetic geometry and the Langlands program. Buzzard's 2017 launch of the Xena Project at Imperial, originally an effort to translate undergraduate mathematics exam problems into Lean exercises, brought a new constituency of pure mathematicians into Mathlib at a moment when the library was still small and largely a computer-science project. The Xena Project's early successes in group theory, ring theory, and analysis seeded a generation of mathematician-formalizers, several of whom later became Mathlib maintainers.[^39][^40]
Buzzard has been an outspoken public advocate for formalization, giving an invited lecture at the 2022 International Congress of Mathematicians on "The rise of formalism in mathematics" and running a long-standing blog at xenaproject.wordpress.com that documents both technical milestones and the cultural reception of formalization among working mathematicians.[^41] His 2024 EPSRC-funded FLT project is the most visible single project in current formalization, and his 2025 grant from the AI for Math Fund supports AI-assisted formalization work.
Beyond Buzzard, the formalization movement involves prominent contributors including Patrick Massot (Paris-Saclay, differential topology and the Blueprint tool), Mario Carneiro (CMU, lead infrastructure work), Johan Commelin (Heidelberg, algebraic geometry and LTE), Floris van Doorn (formal mathematics), Sébastien Gouëzel (dynamical systems), Heather Macbeth (differential geometry), Kim Morrison (topology and category theory), and roughly 30 active maintainers alongside hundreds of occasional contributors.[^26]
Mathlib's community infrastructure rests on three pillars: GitHub for code and pull requests, a public Zulip chat instance for real-time conversation, and the leanprover-community.github.io website for documentation, statistics, and onboarding. The Lean community Zulip is widely cited as the social glue of the project; its topic-based threading allows newcomers to ask basic questions in clearly demarcated streams without disrupting research-level discussions.[^42][^43]
The community is geographically distributed across North America, Europe, Australia, and East Asia, with no central institution. Carnegie Mellon, Imperial College London, Université Paris-Saclay, Heidelberg, and Bonn have hosted clusters of active contributors and workshops, but no single university or company controls the project. The Apache 2.0 license ensures that all contributions are permissively redistributable.[^2]
Yearly Lean Together workshops and topical workshops at venues such as the Hausdorff Center, the Hoskinson Center at CMU, and the Institute for Advanced Study have served as in-person coordination points.[^28]
Mathlib is one of several large libraries developed for proof assistants. Precise size comparisons are difficult because different libraries count differently, but the qualitative landscape is established.[^44]
Among these, Mathlib is generally considered the largest and most rapidly growing as of the mid-2020s. The combination of dependent type theory, classical-logic conventions, automation, and a vibrant community has positioned it as the default target for both formalization and AI proof systems.[^44]
Per the Mathlib project's own statistics page (mathlib_stats.html), as of 2026 the library contained:[^3]
Earlier reference points reported by the project and by Lean Lang's case-study page include:[^3][^4][^34]
Because of the project's pace of change, any specific number reported in the literature should be read with its date attached. The Mathlib statistics page is updated automatically and provides the most current values.[^3]
Mathlib's trajectory across nearly a decade illustrates a transition in the social structure of pure mathematics. What began as a niche project among programming-language researchers has become a publicly funded shared infrastructure with hundreds of contributors, named donors at the multi-million-dollar level, and a privileged role in the training of AI systems that increasingly produce mathematics of their own.