Theorem Proving
Learn to write mathematical proofs in Lean 4. Understand propositions, proof terms, and the tactics that construct them.
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 master the core tactics in Module 2; they power almost every proof you will write. 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 essential 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 fundamental tactics built into Lean 4. Master 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?