Source-linked AI summary
The Lean mathematical library
The mathlib Community
TL;DR
The paper presents mathlib as a community-driven Lean library for formalized mathematics, addressing how such a unified repository can support classical, research-level mathematics. It describes the library’s dependent-type foundations, structure hierarchy, automation, and distributed organization, while identifying analysis as a weaker area.
Problem
Mathlib addresses the challenge of building a unified formal library that supports classical, research-level mathematics and programming in Lean.
Method
The paper analyzes mathlib’s architecture, design decisions, structure hierarchy, automation, and community organization.
Results
Mathlib grew from 15k to 140k lines of code over two years through contributions from 73 people managed by 11 maintainers.
Takeaways & Limitations
Mathlib’s unified development by mathematicians, computer scientists, and programmers has produced a shared library of formalizations and tools used across Lean programming and proving.
Takeaways & Limitations
Analysis is a weaker area of mathlib, although the Fréchet derivative, Bochner integral, and basic trigonometric properties have been formalized.
Abstract
from arXiv · showhide
This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led us here.
1 Introduction
The paper introduces mathlib as a community-driven formal library for Lean, distinguished by its organization, classical mathematical focus, and automation. It explains the design decisions and community practices behind a rapidly growing repository.
- 1 Introduction: The paper is presented under a collective pseudonym because it describes a community effort with 73 contributors.Authorship was not attributed to a subset of contributors.
- 1 Introduction: Mathlib is a formal library for Lean developed by users without a central organization.Its repository emerged from contributors’ desire to develop formal mathematical proofs.
- 1 Introduction: Mathematicians’ participation has shaped mathlib toward formalizing contemporary, research-level mathematics.The paper notes that projects in Section 7.2 suggest this goal is being approached.
- 1 Introduction: Lean’s documentation, classical-mathematics focus, and real-time Zulip chat helped attract users after the core library split from the system repository.The project was initially led by Mario Carneiro and Johannes Hölzl, with a growing user base.
- 1.1 A History of mathlib and Lean 3: Over two years, mathlib grew from 15k to 140k lines of code through contributions from 73 people managed by 11 maintainers.It became the de facto standard library for programming and proving in Lean 3, with supporting community infrastructure and courses.
2 Lean
Lean is based on dependent type theory extended with classical axioms and quotient types. Its metaprogramming framework lets users build tactics and commands that support mathlib’s automation and formalization workflow.
- 2 Lean: Lean uses dependent types based on the calculus of inductive constructions, with a universe hierarchy including Prop and successive Type universes.Prop is impredicative and proof-irrelevant.
- 2 Lean: Lean adds classical.choice and propext, incorporating choice and proposition extensionality into its type theory.classical.choice produces a term from a proof that its type is nonempty, while propext equates logically equivalent propositions.
- 2 Lean: Quotient types identify terms related by an equivalence relation, allowing equality reasoning on quotients without setoids.This supports working directly with quotient objects.
- 2 Lean: Lean’s metaprogramming framework allows tactics, commands, and other environment-manipulating tools to be written in Lean itself.Mathlib uses this framework for powerful automation and specialized commands.
3 Contents of mathlib
Mathlib combines a core programming and proving foundation with broad mathematical libraries covering algebra, topology, analysis, and advanced formalizations. Its contents rely heavily on dependent types, quotients, structure hierarchies, and automation, while analysis remains comparatively weaker.
- 3 Contents of mathlib: Mathlib is designed both for research-level mathematics and as Lean’s standard programming library, building on a 19k-LOC core library.The core provides metaprogramming and tactic infrastructure, algebraic hierarchy, and basic datatypes.
- 3 Contents of mathlib: Its top-level source directories cover algebraic hierarchies, number systems, sets, subtypes, functions, polynomials, lists, multisets, and vectors.The paper presents Table 1 as a rough size comparison of these directories.
- 3 Contents of mathlib: Quotients define structures such as multisets, finite sets, quotient groups, tensor products, colimits, cardinals, and ordinals.They are used throughout algebra, topology, completion constructions, and number systems.
- 3 Contents of mathlib: The topology library includes uniform and metric spaces, topological groups and rings, and the Gromov–Hausdorff space proved to be Polish.The Gromov–Hausdorff space consists of nonempty compact metric spaces up to isometry with its natural distance.
- 3 Contents of mathlib: Mathlib’s manifold definition supports any non-discrete normed field, arbitrary models and structure groupoids, and examples with differentiability, boundaries, or corners.Potential future examples include analytic, contact, symplectic, and translation manifolds.
- 3 Contents of mathlib: Analysis is identified as a weaker area, despite formalizations including the Fréchet derivative, Bochner integral, and basic trigonometric properties.The paper contrasts this limitation with substantial results in algebra, computability, p-adic numbers, topology, and contemporary mathematics.
4 Type Classes
Mathlib uses type classes to organize a broad structure hierarchy, with semi-bundled definitions and bundled morphisms chosen to support inference and formalization. This design provides extensive abstraction but also creates search and matching costs.
- Type classes: Type classes attach predicates or data to types and are inferred by Prolog-like backtracking for notation, structures, coercions, and decidability.Mathlib expands this usage throughout the library.
- Organizing the Structure Hierarchy: The structure hierarchy connects algebraic, topological, categorical, and notation classes rather than forming a simple tree.For example, real numbers instantiate several structures, and the hierarchy contains common diamonds.
- Organizing the Structure Hierarchy: 201 unary classes and 266 instances of the form C α →D α populate the current structure hierarchy, whose illustrated fragment is less than one-third of the whole.Most classes have the unary form C α, while some classes are binary, such as module R M.
- Bundling Structures: Mathlib primarily uses semi-bundled type classes, exposing carrier types while bundling operations so canonical structures can be inferred.Fully bundled definitions are unsuitable for type class problems because a type class should have essentially at most one solution.
- Bundling Structures: Further unbundling makes matching difficult and can cause false positives and failed type class searches, especially when simp is invoked.The issue arises because higher-order matching can substitute lambda terms for operations.
- Bundled Morphisms: Bundled morphisms avoid searching for properties of composed functions and make the morphism type itself easier to equip with mathematical structure.Mathlib explicitly defines composition for bundled homs, and linear maps form an R-module under pointwise operations.
- The decidable Type Class: The decidable p type class supplies a Type-valued witness of p or ¬p, allowing propositions to remain primary while supporting computation.Its side condition is managed almost entirely automatically, and ite performs case analysis on the witness.
5 Linear Algebra
Mathlib develops linear algebra through bundled structures, lattice-based submodules, quotient constructions, bases, dimension theory, and matrix–linear-map correspondences. These formalizations support nontrivial theorems, including isomorphism laws and dimension results.
- Modules: Mathlib represents modules, submodules, quotients, linear maps, kernels, and ranges as structured objects with reusable algebraic operations.Submodules form a complete lattice, enabling span and quotient constructions.
- Modules: The module quotient by a submodule is itself an R-module, and linear-map kernels and ranges are represented as submodules.These definitions are used to prove the first and second isomorphism laws for modules.
- Bases and dimension: A basis combines linear independence with spanning, allowing mathlib to define vector decomposition and prove that every vector space has a basis.The existence result uses Zorn’s lemma and is nonconstructive.
- Bases and dimension: Any two bases have equal cardinality, which mathlib uses to define dimension and state dimension theorems across universe levels.The library includes quotient-dimension and rank-nullity results.
- Matrices: For finite bases, spaces of linear maps are linearly equivalent to spaces of matrices, establishing a direct correspondence between abstract maps and matrix representations.Matrices are modeled as functions on finite index types and form R-modules.
6 Metaprogramming
Mathlib uses Lean’s metaprogramming framework to provide automation, proof-search tools, maintenance commands, and specialized tactics without requiring prover plugins. Its design treats tactic development as part of library design.
- Metaprogramming infrastructure: Lean metaprograms in mathlib implement decision procedures, debugging utilities, user commands, attributes, and specialized automation.Only simp, E-matching, and congruence closure are exposed as atomic procedures rather than implemented as metaprograms.
- Simplification: The simp tactic performs directional rewriting, while simp-normal forms ensure equivalent expressions are consistently represented.The reassoc attribute generates companion lemmas for composition under simp’s right-associated normal form.
- Big automation: General-purpose tactics include finish and tidy, while ring, abel, linarith, and omega automate propositional, algebraic, and linear-arithmetic reasoning.linarith is based on Fourier–Motzkin elimination, and omega partially implements Presburger arithmetic on N and Z.
- Small automation: Specialized tools such as norm_cast, norm_num, and pi_instance reduce coercion, arithmetic, and function-space-instance boilerplate.These tools exploit attributes, numeral representations, and type-class generalization.
- Design lessons: Mathlib provides its automation within the library, and collaboration between mathematicians and programmers has shaped tactics around recurring formalization needs.The project explicitly treats tactic and tool development as library design rather than system development.
7 Community
Mathlib is an open-source community project serving research mathematics, education, proof search, and program verification rather than a single project. Its distributed collaboration supports broad formalization efforts and specialized applications.
- Organization: Mathlib’s contributors have diverse motivations, and design decisions are discussed publicly with little central control over content.The project is organized as an open-source community rather than being overseen by a dedicated research group.
- Organization: Collaboration across contributors is presented as vital to designing a library that is both broad and deep.Mathematicians integrate projects with one another and with mathlib rather than building isolated projects on a generic core.
- Education: Lean is being used in mathematics education as mathematicians adopt mathlib, with undergraduates participating in chat, contributions, and review.The paper describes this educational use as a side effect of adoption by mathematicians.
- Applications: Mathlib supports projects ranging from published research formalizations to collaborative weekend efforts, reflecting the community’s varied interests.Examples include formalizations of the cap set problem, the continuum hypothesis, perfectoid spaces, and other results.
- Applications: Formalized decision procedures for modal logics use mathlib’s sublist-permutation support, while termination proofs prompted further list-theory development.The verified procedures cover K, KT, and S4 and are implemented as totally correct Lean programs.
8 Comparison with Other Libraries
The comparison situates mathlib among formal libraries by examining foundations, structure representation, and automation. It contrasts set theory, simple type theory, and dependent type theory, emphasizing trade-offs in expressiveness, hierarchy support, and proof automation.
- Comparison scope: The comparison covers axiomatic foundations, structure hierarchies, and automation across major formal mathematics libraries.The libraries considered include Mizar, HOL Light, Isabelle/HOL, Coq/SSReflect, and Metamath.
- Set theory: Set-theoretic systems offer familiar foundations and simple proof checking, but fully explicit proofs can impose a high burden on users.Metamath uses set theory and has relatively little automation beyond support for well-formedness; explicitness remains a user cost.
- Simple type theory: Simple type theory handles concrete structures well but restricts algebraic reasoning because types cannot depend on object parameters.Parameterized spaces and structures must instead be modeled using predicates on fixed ambient types, while some higher-order structures cannot be formed directly.
- Simple type theory: HOL Light and Isabelle/HOL provide substantial libraries, while Isabelle additionally offers internal automation, decision procedures, rewriting, and proof-reconstructing external provers.HOL Light is especially strong in multivariate and complex analysis; Isabelle’s library and Archive of Formal Proofs are also extensive.
- Dependent type theory: Mathematical Components uses dependent type theory, canonical structures, constructive foundations, and computational verification with little external automation.Its focus includes group theory, linear algebra, and representation theory, and its structure instantiation is generally more conservative than mathlib’s.
9 Conclusion
Mathlib combines dependent types, classical mathematics, automation, and an interconnected structure hierarchy in a distributed, growing community. Its development reflects collaboration across mathematical and computational roles, while migration to a new Lean version remains an uncertain undertaking.
- 9 Conclusion: Mathlib combines dependent type theory, classical mathematics, executable computational content, useful automation, and a large interconnected hierarchy of structures.The paper states that no other discussed library is known to share all these features.
- 9 Conclusion: Mathlib and its surrounding community continue to grow in mathematical content, automated reasoning tools, and infrastructure without a fixed target or end goal.Future development is described as following the needs and desires of community participants.
- 9 Conclusion: A future Lean version will not be backward compatible, and updating mathlib may be difficult to predict in scale despite possible porting automation.Lean 4 is expected to improve metaprogramming through syntax-tree access and a customizable parser.
- 9 Conclusion: The unified library’s special character is attributed to contributions from mathematicians, computer scientists, and programmers learning from one another.The paper presents the combined effort as successful while emphasizing that the community continues to evolve.