Mathlib
In plain wordsA huge shared library of mathematics written in the Lean language, in which every definition and proof has been checked by computer. Mathematicians keep extending it, and AI proof systems are trained on it.
The community-maintained library of formalized mathematics for the LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs. proof assistant, spanning algebra, analysis, topology, number theory, combinatorics, geometry, measure and probability theory, category theory and more, with every proof certified by Lean's kernel. It is a single, continuously integrated code base rather than a collection of separate projects: hundreds of contributors submit changes through peer review, and maintainers refactor constantly so that new results reuse shared, highly general abstractions, such as typeclasses for algebraic structures and filters for limits. As of October 2026 it held about 140,000 definitions and 290,000 theorems. For AI, Mathlib is the main corpus for training neural theorem proversautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement. and the store of lemmas ('premises') they must search, and formal benchmarks such as miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically., ProofNet and PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics. state their problems on top of it. Large human formalization efforts build on it too, including Kevin Buzzard's project, begun in 2024, to formalize the proof of Fermat's Last Theorem.
The prover kept failing because the lemma it needed had been renamed in the latest Mathlib.
Origin
Created in 2017, when the mathematics in Lean 3's standard library was split into a separate community repository, mathlib, with Johannes Hölzl and Mario Carneiro among its first maintainers. Recruitment of mathematicians, notably by Kevin Buzzard at Imperial College London, drove rapid growth. It was ported to Lean 4 as Mathlib (repository mathlib4), a migration completed in 2023.
Usage note
Lowercase 'mathlib' usually refers to the Lean 3 library. Because formalizing even well-known results remains slow and laborious, Mathlib's coverage of research mathematics is uneven, one motivation for autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify. and AI proof assistants.
Related
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
- miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically.
- AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time.
Sources
- The mathlib Community (2020). The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020).
Mentioned in
miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.