Mathlib is a community-maintained mathematical library for the Lean 4 theorem prover. It provides a vast collection of formalized mathematics — from foundational logic and algebra through real and complex analysis, topology, number theory, category theory, and beyond — together with a powerful suite of automation tactics to make proofs shorter and more readable.Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt
Use this file to discover all available pages before exploring further.
Introduction
Learn what Mathlib is, who maintains it, and how it fits into the Lean ecosystem.
Installation
Install Lean 4, Lake, and Mathlib on your system in minutes.
Using as a Dependency
Add Mathlib to your own Lean 4 project and fetch precompiled build cache.
Quickstart
Write your first Lean 4 proof using Mathlib in a few lines of code.
Explore the Library
Mathematics Overview
Survey the mathematical domains covered, from group theory to algebraic geometry.
Tactics
Automate proofs with
linarith, ring, norm_num, simp, omega, positivity, and more.Contributing
Join the community — learn the style guide, naming conventions, and PR workflow.
Library Reference
Browse the module hierarchy, dependencies, and the formalized 100 theorems list.
Why Mathlib?
Comprehensive Coverage
Mathlib contains over 8,000 modules and hundreds of thousands of definitions and theorems. It is the largest single-language formalized mathematics library in the world.
Fast Builds with Precompiled Cache
Run
lake exe cache get to download precompiled .olean files from Mathlib’s CI servers. Incremental builds on a laptop take seconds, not hours.Powerful Automation
Tactics like
linarith, ring, norm_num, simp, and omega discharge routine proof obligations automatically, letting you focus on the interesting parts.Active Community
Hundreds of contributors maintain Mathlib on Zulip. Questions from beginners and experts alike are welcome.
Mathlib targets a fixed Lean 4 toolchain version. When starting a new project, copy the
lean-toolchain file from Mathlib to ensure compatibility. See Using as a Dependency for details.