Theorem Proving
Learn to write mathematical proofs in Lean 4. Understand propositions, proof terms, and the tactics that construct them.
Why Theorem Proving?
In Lean, types can express properties about your code. A function returning Sorted list instead of just List guarantees sortedness at compile time. But to use such types, you need to provethat your code satisfies those properties. Tactics are the tools that help you construct those proofs.
Core Lean 4 Tactics
These tactics are built into Lean 4 and available without any imports.
Introduction to Proofs
Understand what proofs are, why we need them, and how Lean represents mathematical truth.
Core Tactics
The fundamental tactics built into Lean 4. Master these first.
Built-in Automation
Automation tactics that ship with Lean 4 core.
Advanced Core
Powerful core tactics for complex proof engineering.
Mathlib4 Tactics
These tactics require import Mathlib.Tactic or specific Mathlib imports. Add Mathlib to your project with lake add mathlib.
Mathlib Arithmetic
Powerful tactics for algebra, arithmetic, and mathematical reasoning.
Mathlib Structural
Pattern matching, extensionality, and proof structure tactics.
Start Here
New to theorem proving? Begin with understanding what proofs actually are and why Lean needs them.
What is a Proof?