Documentation overview

This page is intended to contain a complete overview of all documentation helpful for users of Mathlib and of Lean in general. We organize the documentation according to the Divio documentation system into four quadrants:

Tutorials are lessons that take you by the hand through a series of steps to complete a project of some kind.

How-to guides take you through the steps required to solve a real-world problem.

Reference guides are complete technical descriptions of the machinery and how to operate it.

Explanations clarify and illuminate a particular topic.

If you have some documentation and it is missing from the list, you can add it to documentation.yaml in the website repository. If you are missing documentation, you can request it on Zulip.

Filter by all tags:

analysis (4) category theory (3) differential geometry (2) elementary (14) euclidean geometry (1) linear algebra (4) logic (12) measure theory (2) probability (1) ring theory (5) topology (5) declarations (21) development (13) classes (18) linters (2) metaprogramming (7) tactics (15) programming (2) teaching (1) incomplete (1) nonmathlib (2) normative (4)

Tutorials

Natural Numbers Game

by Kevin Buzzard, Jon Eugster, Mohammad Pedramfar, Alexander Bentkamp, Patrick Massot

An online tutorial for everyone who wants to try out Lean. Proving elementary properties on natural numbers.

Glimpse of Lean

by Patrick Massot

An introduction to theorem proving in Lean for the impatient. Get a feel for proving real theorems in Lean in a few hours.

Mathematics in Lean

by Jeremy Avigad, Patrick Massot

The standard textbook on getting started with formalizing maths in Lean.

Mechanics of Proof

by Heather Macbeth

Textbook on writing careful, rigorous mathematical proof. Aimed at readers with less mathematical experience than Mathematics in Lean.

Theorem Proving in Lean 4

by Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich

Introductory textbook for Lean, more focussed on the foundations of type theory.

The Hitchhiker's Guide to Logical Verification

by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg

Textbook for computer science and program verification using Lean.

Logic and Proof

by Jeremy Avigad, Joseph Hua, Robert Y. Lewis, Floris van Doorn

Textbook on mathematical logic using Lean and natural deduction.

The equation compiler and WellFoundedRelation

by the Mathlib community

A walkthrough on the use of well-founded recursion to show termination of the gcd algorithm.

Introduction to Tactic Writing in Lean

by Mirek Olšák

Tutorials for tactic writing, in increasing level of difficulty.

How-to guides

Mathlib Manual: Guides: Shared Mathlib installation

by Jon Eugster

A trick to not download different Mathlib installations for each of your Lean projects.

Mathlib Manual: Guides: Follow Stable Dependencies

by Jon Eugster

A trick to specify only stable releases of your dependencies in the Lakefile.

Mathlib Manual: Guides: Using local dev version of a dependency

by Jon Eugster

A trick to use local copies of a repository for development.

How to use calc

by the Mathlib community

A guide to writing computational proofs using the calc environment.

How to speed up a Mathlib file

by the Mathlib community

Tips and tricks to fix a file that compiles slowly.

How to contribute to Mathlib

by the Mathlib community

How-to guide for contributors to Mathlib.

Git Guide for Mathlib4 Contributors

by the Mathlib community

How-to guide for making effective use of Git, focussed on contributing to Mathlib.

Pull Request Review Guide

by the Mathlib community

How to write a good review for pull requests to Mathlib. For everyone, not just members of the maintainer team.

library note [custom simps projection]

by the Mathlib community

How to register projections for the @[simps] attribute.

Metaprogramming for dummies

by the Mathlib community

A basic introduction to metaprogramming in Lean.

Metaprogramming gotchas

by the Mathlib community

Lists common bugs in tactic writing for Lean.

Setting up linting and testing for your Lean project

by the Mathlib community

How to add a linting and testing framework to a math project in Lean.

Formalizing mathematics: How to format your code well

by Bhavik Mehta

Guide to writing well-formatted Lean code according to the Mathlib style guidelines.

Reference guides

Lean 4 tactic cheatsheet

by the Mathlib community

Cheatsheet for the most common tactics.

Mathlib API documentation

by the Mathlib community

A complete listing of all definitions and theorems included with Mathlib.

Loogle

by Joachim Breitner

Search tool for Lean/Mathlib declarations.

Foundational types

by the Mathlib community

Documents the types built into the foundations of Lean.

The Lean Language Reference

by the Lean developers

A complete description of the features included in core Lean.

Lean Glossary

by the Mathlib community

Explanations of terminology one might encounter in the Lean community.

Mathlib Manual: Tactics

by the Mathlib community

Documentation on tactics included with Mathlib, including a complete index.

A mathlib overview

by the Mathlib community

A index of Mathlib organized by mathematical topic.

Undergraduate mathematics in Mathlib

by the Mathlib community

An index of undergraduate mathematical topics available in Mathlib.

100 theorems

by the Mathlib community

Indexes which of Freek Wiedijk's 100 classical theorems have been formalized in Mathlib.

1000+ theorems

by the Mathlib community

Indexes further famous theorems with formalization in Mathlib.

Maths in Lean: the natural numbers

by the Mathlib community

Overview of the theory of natural numbers in Lean and Mathlib.

Maths in Lean: linear algebra

by the Mathlib community

Overview of the theory of linear algebra in Mathlib.

Maths in Lean: Sets and set-like objects

by the Mathlib community

Overview of the theory of sets, lists and more in Mathlib.

Maths in Lean: Topological, uniform and metric spaces

by the Mathlib community

Overview of the theory of topology in Mathlib.

Maths in Lean: category theory

by the Mathlib community

Overview of category theory in Mathlib.

Mathlib naming conventions

by the Mathlib community

Defines how Mathlib names declarations in a systematic way.

Library style guidelines

by the Mathlib community

Defines how to format code to contribute to Mathlib.

Documentation style guidelines

by the Mathlib community

Defines how to write documentation for your contributions to Mathlib.

Pull request title and description conventions

by the Mathlib community

Defines the writing style of text in a pull request for contributions to Mathlib.

The Lean Github ecosystem

by the Mathlib community

Overview of the development flow for branches in the Lean ecosystem.

The monad map

by the Mathlib community

Overview of the metaprogramming monads in Lean.

Formalizing mathematics: Tactics

by Bhavik Mehta

Overview of the most important tactics made available by Mathlib.

Explanations

Tips and suggestions for teaching with Lean

by the Mathlib community

Strategies and approaches for teaching with Lean

The conversion tactic mode

by the Mathlib community

A guide to writing calculation proofs using the conv environment.

Simplifier

by the Mathlib community

Basic usage and pitfalls for the simp and dsimp tactics.

Common Lean Pitfalls

by the Mathlib community

How to avoid mistakes commonly made by Lean users.

What is a quotient?

by Kevin Buzzard

How quotients work in Lean, compared to quotients in (naïve) set theory.

Division by zero in type theory: a FAQ

by Kevin Buzzard

Explains why Lean chooses to define that 1 / 0 = 0.

library note [the algebraic hierarchy]

by the Mathlib community

Explains the structure of the algebraic hierarchy and how to add new elements to it.

library note [reducible non-instances]

by the Mathlib community

Definitions that cannot be instances should be made reducible.

library note [implicit instance arguments]

by the Mathlib community

Some places prefer implicit {} brackets for typeclass arguments instead of typical instance [] brackets.

library note [lower instance priority]

by the Mathlib community

When creating an instance that always applies, give it a lower priority.

library note [instance argument order]

by the Mathlib community

A trick to speed up typeclass instance synthesis by putting more specific goals first.

library note [SetLike Aesop ruleset]

by the Mathlib community

How to add rules about SetLike membership to Aesop.

library note [no_index around OfNat.ofNat]

by the Mathlib community

Write ofNat(n) in lemmas instead of OfNat.ofNat n.

library note [coercion into rings]

by the Mathlib community

How to set up coercions from a concrete structure like ℕ to an arbitrary ring R.

library note [RCLike instance]

by the Mathlib community

An instance creating a goal [RCLike ?m] is okay since there are only two choices, ℝ or ℂ.

library note [fact non-instances]

by the Mathlib community

We do not declare any global instances of the Fact typeclass.

library note [decidable namespace]

by the Mathlib community

The Decidable namespace contains theorems that avoid the use of the Law of Excluded Middle by using Decidable instances instead.

library note [decidable arguments]

by the Mathlib community

If a Decidable hypothesis is not needed for the type signature of a theorem or lemma, use classical instead.

library note [slow-failing instance priority]

by the Mathlib community

Instances that would be slow to fail to apply should have a lower priority.

library note [foundational algebra order theory]

by the Mathlib community

Batteries sets up the algebraic and order theoretic properties of Nat and Int; Mathlib replaces this with a typeclass-based system.

library note [continuity lemma statement]

by the Mathlib community

How to write more useful continuity lemmas.

library note [comp_of_eq lemmas]

by the Mathlib community

How to avoid elaboration problems when writing the continuity of a composition.

library note [IMO geometry formalization conventions]

by the Mathlib community

Conventions for formalizing geometry problems from the IMO as part of Mathlib's Archive.

library note [change elaboration strategy with `by apply`]

by the Mathlib community

A trick to elaborate a term and its type in a different order.

library note [pointwise nat action]

by the Mathlib community

The action of natural numbers or integers on sets takes precedence over pointwise actions.

library note [Design choices about smooth algebraic structures]

by the Mathlib community

Mathlib's design choices about smooth algebraic structures

library note [Manifold type tags]

by the Mathlib community

Explains why ModelProd and ModelPi exist.

library note [non-Archimedean non-instances]

by the Mathlib community

Why non-Archimedean subgroup basis lemmas cannot be instances.

library note [range copy pattern]

by the Mathlib community

The image of a morphism f is defined using Set.range if possible, not map ⊤ f.

library note [continuous functional calculus]

by the Mathlib community

Design overview of the ontinuous functional calculus in Mathlib.

library note [specialised high priority simp lemma]

by the Mathlib community

When not to un-@[simp] a lemma in favour of a more powerful version.

library note [out-param inheritance]

by the Mathlib community

Limitations on the interaction of typeclass inheritance and outParams.

library note [lower cancel priority]

by the Mathlib community

Inheritance from cancellative algebraic structures gets a lower priority.

library note [forgetful inheritance]

by the Mathlib community

Design pattern for typeclass inheritance where we include all fields, even if they can be inferred.

library note [norm_num lemma function equality]

by the Mathlib community

Why lemmas for the norm_num tactic use a parameter f and hypothesis f = HAdd.add instead of writing +.

library note [hom simp lemma priority]

by the Mathlib community

Widely applicable @[simp] lemmas should receive mid priority.

library note [CategoryTheory universes]

by the Mathlib community

Design patterns for ordering the universe levels in category theory declarations.

library note [operator precedence of big operators]

by the Mathlib community

The choice of operator precedence for ∏ and ∑ operators in Mathlib.

library note [bundled maps over different rings]

by the Mathlib community

A design trick for when bundled maps have stronger properties if certain typeclass assumptions are satisfied.

Computation models for polynomials and finitely supported functions

by the Mathlib community

An overview of potential (re)implementations for computable polynomials in Mathlib.

Tradeoffs of concrete types defined as subobjects

by the Mathlib community

Reasons to prefer defining something as a custom structure, a coercion to Type, or a subobject.

Formalizing mathematics: Types and terms

by Bhavik Mehta