Mathlib Manual🔗

This document has been last updated at 2025-03-07 14:53 (+0000) using Lean 4.17.0 and Mathlib commit 5269898.

Other resources:

If you would like to contribute content, please create a PR using the two github links at the bottom left of this page!

  1. 1. Tactics
    1. 1.1. Interactive
    2. 1.2. Automation
    3. 1.3. Algebra
    4. 1.4. Analysis
    5. 1.5. Coercions
    6. 1.6. Category Theory
    7. 1.7. Logic
    8. 1.8. Induction / case distinction
    9. 1.9. Basic tactics / assumptions
    10. 1.10. Definitional equality
    11. 1.11. Conv mode
    12. 1.12. Control flow
    13. 1.13. For Tests
    14. 1.14. Miscellaneous
    15. 1.15. All tactics
  2. 2. Guides
    1. 2.1. Shared Mathlib Installation
    2. 2.2. Follow Stable Dependencies
    3. 2.3. Using local dev version of a dependency