Theorem Proving
Writing proofs in Lean 4: what a proof is, how to read the proof state, and the tactics that build proofs.
Tactics are a guided way to build proof terms. Each tactic transforms the proof state: it introduces assumptions, splits goals, rewrites targets, or closes goals entirely. This section teaches the core moves and how to combine them into reliable proof workflows.
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 let you build those proofs interactively, one focused step at a time, until no goals remain.
How to Use This Section
Start with Module 1 to learn how to read the proof state. Then learn the core tactics in Module 2; almost every proof uses them. From there, add automation and advanced structuring tools as you need them.
Proof Workflow
- Introduce assumptions and variables with
intro. - Split goals with
casesandinduction. - Rewrite and simplify using
rwandsimp. - Close goals with
exact,apply, or automation.
Topic Map
- Goal management and structure:
have,cases,induction. - Automation:
decide,omega,aesop. - Large proofs:
calc,conv, combinators. - Mathlib power tools:
ring,linarith,ext.
Core Lean 4 Tactics
These tactics are built into Lean 4 and available without any imports. They cover the basic moves: introducing hypotheses, rewriting goals, splitting cases, and closing proofs.
Introduction to Proofs
Understand what proofs are, why we need them, and how Lean represents mathematical truth.
Core Tactics
The tactics built into Lean 4. Learn these first.
Automation
Automation tactics for routine proofs, from core tools to Mathlib search.
Advanced Core
Powerful core tactics for complex proof engineering and strategy.
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?