Primary evidence
- leanprover-community/mathlib3 repositoryS1 · Primary research · Repository
- The Lean mathematical libraryS1 · Primary research · Paper · 2019-10-21
Mathlib3 creates a shared Lean library for collaborative formal mathematics
Mathlib organized community-authored Lean definitions, theorems, proofs and tactics into a common mathematical library spanning algebra, analysis, topology, number theory and other areas. Shared APIs and review practices made formal developments composable rather than isolated project artifacts.
What happened?
The preserved leanprover-community/mathlib3 repository was created on GitHub on 21 July 2017, providing the exact artifact anchor used for this Event. The later mathlib community paper documents the project as a community-driven effort to build a unified library of mathematics formalized in Lean and explains its mathematical, automation and organizational architecture.
Why it matters
Modern learning-based theorem provers need not only a proof checker but also large libraries of formal statements, proof states and dependencies. Mathlib became precisely that substrate for Lean, later underpinning environments and datasets such as LeanDojo and a wide range of LLM-based formal-math systems.
Significance rationale: Mathlib transformed Lean from a proof-assistant platform into a growing shared corpus of reusable formal mathematics. The library's scale, collaborative development model and machine-readable theorem/proof data later made it central infrastructure for Lean-based AI theorem proving and benchmark construction.
Historical context
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Claimed
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The mathematical library was primarily authored and reviewed by humans, while Lean mechanically checked the formal content; the Event concerns creation of machine-readable proof infrastructure rather than autonomous AI discovery.
- Human contribution
- The Lean mathematical community collaboratively developed, reviewed and maintained reusable formal definitions, theorems, proofs and automation in a shared repository.
- Verification
- Claimed · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-27
Technical details
- Systems
- lean, mathlib3
- Organizations
- leanprover-community
- Problems
- formal-mathematical-knowledge
- Methods
- mathematical-library, collaborative-formalization, proof-checking, interactive-theorem-proving
Sources & artifacts
- leanprover-community/mathlib3 repositoryS1 · Primary research · Repository · accessed 2026-09-15
- The Lean mathematical libraryS1 · Primary research · Paper · accessed 2026-09-15
- Lean 3 mathlib repositoryArtifact · Code
Verification history
- 2017-07-21 · Claimed · E3 · Inspectable artifact
The preserved public repository provides an exact GitHub creation timestamp and directly inspectable formal artifact; the later mathlib paper documents the library's community-driven architecture and scope.
Corrections
No corrections recorded.