Lean 101: from a mathematical argument to a checked proof
For anyone who has met proofs, in mathematics, in physics or any other science, or simply for the pleasure of them: the arguments you already know, written so that Lean checks them.
This tutorial runs on your own Lean installation, with Mathlib. Tools ▸ Check CAS and AIs shows whether Lean is ready on this computer; Help ▸ How to ▸ Setting up Lean describes the installation.
This page reproduces exactly what the Workspace shows at Help > Tutorials > Lean 101, with the results of its own run. With the Workspace and Lean installed on your computer, every input in the Workspace runs live: an example can be changed and checked again, a proof can be taken in another direction, and each exercise can be tried before its solution is opened. ← Lean in the Workspace
What Lean brings
A proof on paper counts on its reader to fill in the types, some of the small cases, etc. Some of them Lean infers, but generally Lean needs more of them explicit, stated by you clearly. Then Lean does four things, in one continuous flow that mirrors what we do with paper and pencil:
States the claim → Shows goals → Proves → Checks
- States the claim.
In Lean. The claim is written as an exact proposition.
Lean words.theorem,lemma,example.
What Lean adds. Before the proof begins, the exact claim is fixed, including its objects, types, assumptions and quantifiers. - Shows goals.
In Lean. When Enter is pressed, Lean checks the input and shows the first goal, the claim itself.
Lean words.:= by.
What Lean adds. At every stage, the exact goals and the available hypotheses are shown. A step missing from the proof leaves its goal open, in view, and the proof is reported incomplete. - Proves.
In Lean. The proof is constructed step by step.
Lean words. Tactics such asintro,exact,constructor,rw,simp,ringandinduction.
What Lean adds. As the proof is written, every step must fit a current goal and becomes part of the complete proof. - Checks.
In Lean. Checks the completed proof against the exact claim.
Lean words. None: every Enter checks.#print axiomsshows what a checked result rests on.
What Lean adds. When no goals remain, Lean independently verifies the finished proof. Later proofs in the same document can cite it by name.
Two supporting activities can enter anywhere they are needed:
- Defines, when needed.
In Lean. A new object or function receives a name and an exact definition.
Lean words.def; later,structureandinductive.
What Lean adds. From its definition onward, the name keeps one exact meaning. Lean can replace the name with the definition in a computation or proof. - Computes, when needed.
In Lean. Lean evaluates a value or reduces an expression when a calculation is useful.
Lean words.#eval; in proofs,rflandnorm_num.
What Lean adds. A computation used inside a proof is part of the checked proof. A value Lean computes with#evalis displayed when the computation is successful.
You can define and compute throughout the work, or even need to do so, in support of Lean’s central contribution: the checked proof.
What Lean computes
- With
#eval, Lean runs the computation and displays the value: exact integer and rational arithmetic of any size (), gcd, remainders, powers, integer factorization (Nat.primeFactorsList 360gives ), primality tests. A real number such as , or a polynomial as Mathlib defines it, has no value to display. - Inside a proof, tactics compute to build the proof:
rflanddecidesettle closed facts on and ();norm_numnumerical facts in any number system, primality included ( is prime);ringpolynomial identities of any degree, andfield_simpfractions with nonzero denominators;linarith,nlinarith,positivityandomegainequalities and linear arithmetic;simprewriting with Mathlib’s lemmas. - Solving equations, factoring polynomials, integrals, limits and series are the CAS’s part: the CAS finds, and Lean checks what it found (section 13).
Approaching Lean
A short, familiar argument is enough to begin learning Lean: its statement gives the first goal, and each familiar move changes that goal. The change explains what the Lean word did. A small working vocabulary comes first; Help ▸ Command help supplies the rest when a new mathematical move demands it.
The comparison with paper is also where the differences become useful. When Lean asks for a type, a missing case or a justification that paper omitted, it is exposing the information that makes the final check possible.
What to expect
By the end, you will have followed the complete proof cycle through genuine number-theory examples: remainders, divisibility, greatest common divisors, sums of two squares, inequalities, Pell equations, the Euclidean algorithm, polynomial patterns, finite sums and Pythagorean triples.
The mathematics gives each Lean action a purpose. The goals then make an unfamiliar proof readable and the next move discoverable.
How to use this tutorial
- Every section ends with an Exercise, and its Solution, collapsed under it, is live like everything here: it runs, it reproduces its result on the Lean on this computer, and it can be edited and run again. The paper argument can come first.
- Enter checks the selected input. Shift+Enter adds a line inside it.
- An input at rest is shown typeset; a click opens its source, as typed, with the cursor where the click landed, and Enter typesets it again.
Natand are the same to Lean. - A backslash and a name, then a space or Tab, give a symbol, with the names VS Code uses:
\and,\or,\to,\forall,\exists,\ne,\ge,\R,\N,\.the bullet ·,\<\>the angle brackets ⟨ ⟩. The Math button in the toolbar opens the palette: in a Lean input it shows Tactics and Symbols, and its search accepts a name, a symbol or a\abbreviation. - Names introduced in an earlier input are available below it.
- The results shown were produced when the tutorial was made, and their badges say Saved check; Enter checks an input again, on the Lean on this computer.
- After a check, the steps of a proof appear below it, each with its goals. An edit in one of those steps changes the proof above at once, and its goals are outdated until the next Enter; after an edit to the proof itself, the steps below are read-only until it is checked again.
- The goal after each line is the most direct explanation of what that line did.
- A goal may carry a line
caseand a name: Lean’s name for that goal, from the step that made it (hafteruse;leftandrightafterconstructor;inlandinrafterrcaseson an “or”). - F1 with the cursor on a Lean word (
theorem,ring,linarith…) opens its help page: its forms, a description, and examples that run. On a name from Mathlib, such asNat.exists_infinite_primes, it shows the statement and documentation that the Lean on this computer has for it. Help ▸ Command help opens the same pages by search. - Mathlib needs no
import Mathlib: the Workspace starts loading it when a Lean document opens, and until it is loaded an input is checked with Lean alone. Tools ▸ Check CAS and AIs ▸ Lean shows the Lake project and toolchain in use, and chooses another project. - An input changed while exploring comes back with Undo.
The palette in a Lean input, on its Symbols tab. The first row is the logic Lean’s statements are made of: for all, there exists, not, and, or, implies, if and only if, true, false. 
The chip at the top right reads lean → lean: the document is written in Lean and checked by Lean. Mathlib supplies the established definitions and theorems used here.
1. State the claim, then read the goal
On paper: a claim is stated in words and symbols; the number system and the operations are understood from the context.
In Lean: the sentence is written as an exact claim, including the number system and the operation being used.
Example
Fermat’s little theorem at , : .
Lean words:
theorem states the claim; := by opens its proof; rfl closes an equality that Lean can obtain directly by reduction.theorem fermat_two_mod_101 : 2^100 % 101 = 1 := by
rflProof checked: fermat_two_mod_101
theorem fermat_two_mod_101 : 2^100 % 101 = 1 := by⊢ 2 ^ 100 % 101 = 1
rfl
No goals
What Lean adds: the claim appears as the first goal. With
rfl, Lean computes , a 31-digit number, and its remainder; no goal remains, and the Workspace reports Proof checked for this exact statement.Exercise
Prove that , Fermat’s little theorem at .
Solution
theorem fermat_three_mod_17 : 3^16 % 17 = 1 := by
rflProof checked: fermat_three_mod_17
theorem fermat_three_mod_17 : 3^16 % 17 = 1 := by⊢ 3 ^ 16 % 17 = 1
rfl
No goals
2. Assume, then conclude
On paper: “Assume . Then … .”
In Lean: an implication begins as a goal;
intro moves into the hypotheses, under a name.Example
For integers , prove that implies . In Lean, means there is an integer with .
Lean words:
intro names the assumption; obtain exposes its factor; use supplies the factor for the conclusion; rw and ring finish the equality.theorem divides_product (a b c : ℤ) : a ∣ b → a ∣ b*c := by
intro h
obtain ⟨k, hk⟩ := h
use k*c
rw [hk]
ringProof checked: divides_product
theorem divides_product (a b c : ℤ) : a ∣ b → a ∣ b*c := bya b c : ℤ
⊢ a ∣ b → a ∣ b * c
intro h
a b c : ℤ
h : a ∣ b
⊢ a ∣ b * c
obtain ⟨k, hk⟩ := h
a b c k : ℤ
hk : b = a * k
⊢ a ∣ b * c
use k*ccase h
a b c k : ℤ
hk : b = a * k
⊢ b * c = a * (k * c)
rw [hk]
case h
a b c k : ℤ
hk : b = a * k
⊢ a * k * c = a * (k * c)
ring
No goals
What Lean adds: after
intro h, obtain reveals an integer with . The witness proves that also divides .Exercise
For integers , prove that and imply .
Solution
theorem divides_sum (a b c : ℤ) : a ∣ b → a ∣ c → a ∣ (b+c) := by
intro hab hac
obtain ⟨k, hk⟩ := hab
obtain ⟨l, hl⟩ := hac
use k+l
rw [hk, hl]
ringProof checked: divides_sum
theorem divides_sum (a b c : ℤ) : a ∣ b → a ∣ c → a ∣ (b+c) := bya b c : ℤ
⊢ a ∣ b → a ∣ c → a ∣ b + c
intro hab hac
a b c : ℤ
hab : a ∣ b
hac : a ∣ c
⊢ a ∣ b + c
obtain ⟨k, hk⟩ := hab
a b c : ℤ
hac : a ∣ c
k : ℤ
hk : b = a * k
⊢ a ∣ b + c
obtain ⟨l, hl⟩ := hac
a b c k : ℤ
hk : b = a * k
l : ℤ
hl : c = a * l
⊢ a ∣ b + c
use k+lcase h
a b c k : ℤ
hk : b = a * k
l : ℤ
hl : c = a * l
⊢ b + c = a * (k + l)
rw [hk, hl]
case h
a b c k : ℤ
hk : b = a * k
l : ℤ
hl : c = a * l
⊢ a * k + a * l = a * (k + l)
ring
No goals
3. Split a claim, or choose a side
On paper: “we prove both parts” for an “and”; “it is enough to prove one of them” for an “or”.
In Lean: an “and” becomes two goals, one for each part; an “or” asks which side is being proved.
Example
If divides both and , then divides and .
Lean words:
constructor creates the two goals; h.1 and h.2 are the two facts contained in the hypothesis; exact closes a goal with a fact that matches it; dvd_add and dvd_sub are Mathlib’s results for a sum and a difference (section 5 says more about citing results); left or right chooses a side of an “or”.theorem common_divisor_sum_difference (a b d : ℤ) (h : d ∣ a ∧ d ∣ b) :
d ∣ a + b ∧ d ∣ a - b := by
constructor
· exact dvd_add h.1 h.2
· exact dvd_sub h.1 h.2Proof checked: common_divisor_sum_difference
theorem common_divisor_sum_difference (a b d : ℤ) (h : d ∣ a ∧ d ∣ b) :
d ∣ a + b ∧ d ∣ a - b := bya b d : ℤ
h : d ∣ a ∧ d ∣ b
⊢ d ∣ a + b ∧ d ∣ a - b
constructor
case left
a b d : ℤ
h : d ∣ a ∧ d ∣ b
⊢ d ∣ a + b
case right
a b d : ℤ
h : d ∣ a ∧ d ∣ b
⊢ d ∣ a - b
· exact dvd_add h.1 h.2
case right
a b d : ℤ
h : d ∣ a ∧ d ∣ b
⊢ d ∣ a - b
· exact dvd_sub h.1 h.2
No goals
What Lean adds: after
constructor, Lean displays the two divisibility claims separately. Each closes with the corresponding Mathlib result applied to the two parts of h.Exercise
For a real number with , prove or .
Solution
theorem square_is_four (x : ℝ) (h : x^2 = 4) : x = 2 ∨ x = -2 := by
have h' : (x - 2) * (x + 2) = 0 := by ring_nf; linarith
rcases mul_eq_zero.mp h' with h1 | h1
· left
linarith
· right
linarithProof checked: square_is_four
theorem square_is_four (x : ℝ) (h : x^2 = 4) : x = 2 ∨ x = -2 := byx : ℝ
h : x ^ 2 = 4
⊢ x = 2 ∨ x = -2
have h' : (x - 2) * (x + 2) = 0 := by ring_nf; linarithx : ℝ
h : x ^ 2 = 4
h' : (x - 2) * (x + 2) = 0
⊢ x = 2 ∨ x = -2
rcases mul_eq_zero.mp h' with h1 | h1
case inl
x : ℝ
h : x ^ 2 = 4
h' : (x - 2) * (x + 2) = 0
h1 : x - 2 = 0
⊢ x = 2 ∨ x = -2
case inr
x : ℝ
h : x ^ 2 = 4
h' : (x - 2) * (x + 2) = 0
h1 : x + 2 = 0
⊢ x = 2 ∨ x = -2
· left
case inl
x : ℝ
h : x ^ 2 = 4
h' : (x - 2) * (x + 2) = 0
h1 : x - 2 = 0
⊢ x = 2
linarith
No goals
· right
case inr
x : ℝ
h : x ^ 2 = 4
h' : (x - 2) * (x + 2) = 0
h1 : x + 2 = 0
⊢ x = -2
linarith
No goals
New words, each used once here.
have states and proves an intermediate fact, : ring_nf multiplies out the product, and linarith (section 8) finishes from h. mul_eq_zero is Mathlib’s result that a product is zero exactly when one of its factors is. rcases splits that “or” into its two cases; in each, left or right chooses the side of the conclusion, and linarith closes it.4. Replace equal things by equal things
On paper: “replacing by its equal …”: substituting equals for equals.
In Lean: rewriting uses an equality to replace one side by the other inside the goal, and shows the goal after the replacement.
Example
The step of Euclid’s algorithm: if , then .
Lean words:
rw [h] replaces using h; rw [← h] replaces in the opposite direction; simp applies Mathlib’s simplification rules; Nat.gcd is the greatest common divisor of two natural numbers, as Mathlib defines it.theorem euclid_step (a b n r : ℕ) (h : a = n*b + r) :
Nat.gcd a b = Nat.gcd r b := by
rw [h]
simpProof checked: euclid_step
theorem euclid_step (a b n r : ℕ) (h : a = n*b + r) :
Nat.gcd a b = Nat.gcd r b := bya b n r : ℕ
h : a = n * b + r
⊢ a.gcd b = r.gcd b
rw [h]
a b n r : ℕ
h : a = n * b + r
⊢ (n * b + r).gcd b = r.gcd b
simp
No goals
What Lean adds: rewriting turns the goal into .
simp knows that adding a multiple of does not change a gcd with , and closes it.Exercise
If and divides both and , prove that divides .
Solution
theorem divides_remainder (a b n r k : ℤ) (h : a = n*b + r) (ha : k ∣ a) (hb : k ∣ b) :
k ∣ r := by
have hr : r = a - n*b := by rw [h]; ring
rw [hr]
exact dvd_sub ha (dvd_mul_of_dvd_right hb n)Proof checked: divides_remainder
theorem divides_remainder (a b n r k : ℤ) (h : a = n*b + r) (ha : k ∣ a) (hb : k ∣ b) :
k ∣ r := bya b n r k : ℤ
h : a = n * b + r
ha : k ∣ a
hb : k ∣ b
⊢ k ∣ r
have hr : r = a - n*b := by rw [h]; ringa b n r k : ℤ
h : a = n * b + r
ha : k ∣ a
hb : k ∣ b
hr : r = a - n * b
⊢ k ∣ r
rw [hr]
a b n r k : ℤ
h : a = n * b + r
ha : k ∣ a
hb : k ∣ b
hr : r = a - n * b
⊢ k ∣ a - n * b
exact dvd_sub ha (dvd_mul_of_dvd_right hb n)
No goals
have states and proves the intermediate fact (section 3); rw [hr] replaces by it in the goal; exact closes the goal with dvd_sub applied to and to , the latter from dvd_mul_of_dvd_right, Mathlib’s result that a divisor of divides .5. Use a result already known
On paper: “by [a known theorem], …”: citing a result already proved.
In Lean: an established theorem can be the complete proof or can reduce the claim to conditions still needing proof. Mathlib supplies the established results.
Example
Euclid: above every natural number there is a prime.
Lean words:
exact supplies a theorem directly; apply uses a theorem and shows any conditions it still needs as new goals; exact? can suggest a matching result; Nat.Prime is primality of a natural number, as Mathlib defines it, written Nat.Prime p or p.Prime.theorem prime_above (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
exact Nat.exists_infinite_primes nProof checked: prime_above
theorem prime_above (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := byn : ℕ
⊢ ∃ p, n ≤ p ∧ Nat.Prime p
exact Nat.exists_infinite_primes n
No goals
The statement of
Nat.exists_infinite_primes matches the whole goal, so citing it completes the proof: Euclid’s theorem, as Mathlib has it.Euclid’s lemma: if a prime divides , then or .
theorem euclid_lemma (p a b : ℕ) (hp : p.Prime) (h : p ∣ a * b) :
p ∣ a ∨ p ∣ b := by
apply (Nat.Prime.dvd_mul hp).mp
exact hProof checked: euclid_lemma
theorem euclid_lemma (p a b : ℕ) (hp : p.Prime) (h : p ∣ a * b) :
p ∣ a ∨ p ∣ b := byp a b : ℕ
hp : Nat.Prime p
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b
apply (Nat.Prime.dvd_mul hp).mp
p a b : ℕ
hp : Nat.Prime p
h : p ∣ a * b
⊢ p ∣ a * b
exact h
No goals
What Lean adds: Mathlib states Euclid’s lemma as an equivalence,
Nat.Prime.dvd_mul. Applying its forward direction leaves as the only goal; the hypothesis closes it.Exercise
Prove that consecutive natural numbers are coprime: .
Solution
theorem consecutive_coprime (n : ℕ) : Nat.gcd n (n + 1) = 1 := by
simpProof checked: consecutive_coprime
theorem consecutive_coprime (n : ℕ) : Nat.gcd n (n + 1) = 1 := byn : ℕ
⊢ n.gcd (n + 1) = 1
simp
No goals
simp closes it with Mathlib’s result that consecutive natural numbers are coprime.6. Compute when computation settles the point
On paper: a calculation may reveal a value or suggest a general identity.
In Lean: a value may be displayed for exploration, while a mathematical claim receives a proof that Lean checks.
Example
Compute .
Lean words:
#eval displays a computable value; norm_num proves exact numerical claims, unfolding the definitions named in its brackets; ring proves polynomial identities.#eval Nat.gcd 252 10521
Lean displays 21. At this point the value has been computed, but no theorem has been stated.
State the computed value as an exact claim.
theorem gcd_value_252_105 : Nat.gcd 252 105 = 21 := by
norm_num [Nat.gcd]Proof checked: gcd_value_252_105
theorem gcd_value_252_105 : Nat.gcd 252 105 = 21 := by⊢ Nat.gcd 252 105 = 21
norm_num [Nat.gcd]
No goals
What Lean adds: this time the result is a theorem.
norm_num constructs a proof of the gcd equality, and Lean checks it.The Brahmagupta–Fibonacci identity expresses a product of two sums of squares as another sum of two squares.
theorem brahmagupta_fibonacci (a b c d : ℝ) :
(a^2 + b^2) * (c^2 + d^2) =
(a*c - b*d)^2 + (a*d + b*c)^2 := by
ringProof checked: brahmagupta_fibonacci
theorem brahmagupta_fibonacci (a b c d : ℝ) :
(a^2 + b^2) * (c^2 + d^2) =
(a*c - b*d)^2 + (a*d + b*c)^2 := bya b c d : ℝ
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
ring
No goals
After
ring, no goal remains. The checked theorem holds for every real in one universal statement.Exercise
Prove Sophie Germain’s identity .
Solution
theorem sophie_germain_identity (a b : ℝ) :
a^4 + 4*b^4 =
(a^2 - 2*a*b + 2*b^2) * (a^2 + 2*a*b + 2*b^2) := by
ringProof checked: sophie_germain_identity
theorem sophie_germain_identity (a b : ℝ) :
a^4 + 4*b^4 =
(a^2 - 2*a*b + 2*b^2) * (a^2 + 2*a*b + 2*b^2) := bya b : ℝ
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)
ring
No goals
7. Respect the number system
On paper: the context usually tells us whether a calculation uses natural numbers, integers or rational numbers.
In Lean: the number system is written as part of the expression, fixing the meaning of subtraction and division.
Example
First ask for the type of when it is written in the natural numbers.
Lean words:
Nat, Int, Rat and ℝ name common number systems; #check reports an expression’s type.#check (3 - 5 : Nat)3 - 5 : ℕ
Lean reports
Nat. Natural-number subtraction cannot produce a negative number.Evaluate the natural-number expression.
#eval (3 - 5 : Nat)0
Lean displays 0.
Evaluate the same notation in the integers.
#eval (3 - 5 : Int)-2
What Lean adds: Lean displays −2. The written type fixed the meaning before either computation began.
Exercise
Evaluate in the natural numbers and in the rational numbers.
Solution
#eval (7 / 2 : Nat)
#eval ((7 : Rat) / 2)Evaluated
Evaluated
3
7 / 2
8. Carry inequalities from the hypotheses
On paper: “from the hypotheses, the bound follows”: combining given inequalities into a new one.
In Lean: the hypotheses are written in the claim, and the conclusion must follow from them.
Example
For real numbers , the midpoint lies between them.
Lean words:
constructor separates the two inequalities; linarith proves linear consequences over the reals; nlinarith also uses products and squares, given as hints; omega handles linear natural-number and integer arithmetic.theorem midpoint_between (a b : ℝ) (h : a ≤ b) :
a ≤ (a + b) / 2 ∧ (a + b) / 2 ≤ b := by
constructor
· linarith
· linarithProof checked: midpoint_between
theorem midpoint_between (a b : ℝ) (h : a ≤ b) :
a ≤ (a + b) / 2 ∧ (a + b) / 2 ≤ b := bya b : ℝ
h : a ≤ b
⊢ a ≤ (a + b) / 2 ∧ (a + b) / 2 ≤ b
constructor
case left
a b : ℝ
h : a ≤ b
⊢ a ≤ (a + b) / 2
case right
a b : ℝ
h : a ≤ b
⊢ (a + b) / 2 ≤ b
· linarith
case right
a b : ℝ
h : a ≤ b
⊢ (a + b) / 2 ≤ b
· linarith
No goals
What Lean adds:
constructor separates the lower and upper bounds. Each call to linarith uses the same assumption to close one goal.Exercise
For real numbers and , prove .
Solution
theorem two_mul_le_sum_squares (a b : ℝ) : 2*a*b ≤ a^2 + b^2 := by
nlinarith [sq_nonneg (a - b)]Proof checked: two_mul_le_sum_squares
theorem two_mul_le_sum_squares (a b : ℝ) : 2*a*b ≤ a^2 + b^2 := bya b : ℝ
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2
nlinarith [sq_nonneg (a - b)]
No goals
The hint is the step one writes on paper:
sq_nonneg (a - b) is that fact, from Mathlib; nlinarith expands it and combines it with the goal.9. Exhibit an object
On paper: “take ; it has the property”: exhibiting a witness.
In Lean: an existence proof supplies the numbers and then proves that they have the stated property.
Example
There is a prime greater than 100.
Lean words:
use supplies the witnesses; the remaining conditions become goals; norm_num can prove the numerical conditions.theorem exists_prime_above_hundred :
∃ p : Nat, p > 100 ∧ Nat.Prime p := by
use 101
norm_numProof checked: exists_prime_above_hundred
theorem exists_prime_above_hundred :
∃ p : Nat, p > 100 ∧ Nat.Prime p := by⊢ ∃ p > 100, Nat.Prime p
use 101case h
⊢ 101 > 100 ∧ Nat.Prime 101
norm_num
No goals
What Lean adds: after the witness 101 is supplied, the remaining goal contains two facts: and the primality of 101.
norm_num proves both.Exercise
Prove that the Pell equation has an integer solution with .
Solution
theorem pell_has_solution :
∃ x y : ℤ, y > 0 ∧ x^2 - 2*y^2 = 1 := by
use 3, 2
norm_numProof checked: pell_has_solution
theorem pell_has_solution :
∃ x y : ℤ, y > 0 ∧ x^2 - 2*y^2 = 1 := by⊢ ∃ x, ∃ y > 0, x ^ 2 - 2 * y ^ 2 = 1
use 3, 2
case h
⊢ 2 > 0 ∧ 3 ^ 2 - 2 * 2 ^ 2 = 1
norm_num
No goals
10. Write a chain of equalities
On paper: a derivation writes a chain of equalities, each step with its reason.
In Lean: a calculation chain records every intermediate expression and the reason each step holds.
Example
Apply the Euclidean algorithm to and .
Lean words:
calc starts the chain; each := by proves one link; _ repeats the preceding right-hand side.theorem gcd_by_euclid_252_105 : Nat.gcd 252 105 = 21 := by
calc
Nat.gcd 252 105 = Nat.gcd 105 42 := by norm_num [Nat.gcd]
_ = Nat.gcd 42 21 := by norm_num [Nat.gcd]
_ = 21 := by norm_num [Nat.gcd]Proof checked: gcd_by_euclid_252_105
theorem gcd_by_euclid_252_105 : Nat.gcd 252 105 = 21 := by⊢ Nat.gcd 252 105 = 21
calc
Nat.gcd 252 105 = Nat.gcd 105 42 := by norm_num [Nat.gcd]
_ = Nat.gcd 42 21 := by norm_num [Nat.gcd]
_ = 21 := by norm_num [Nat.gcd]No goals
What Lean adds: the
calc block records the successive gcd pairs , and . Lean checks every equality in the chain.Exercise
Use a
calc chain to prove by the Euclidean algorithm.Solution
theorem gcd_by_euclid_240_46 : Nat.gcd 240 46 = 2 := by
calc
Nat.gcd 240 46 = Nat.gcd 46 10 := by norm_num [Nat.gcd]
_ = Nat.gcd 10 6 := by norm_num [Nat.gcd]
_ = Nat.gcd 6 4 := by norm_num [Nat.gcd]
_ = Nat.gcd 4 2 := by norm_num [Nat.gcd]
_ = 2 := by norm_num [Nat.gcd]Proof checked: gcd_by_euclid_240_46
theorem gcd_by_euclid_240_46 : Nat.gcd 240 46 = 2 := by⊢ Nat.gcd 240 46 = 2
calc
Nat.gcd 240 46 = Nat.gcd 46 10 := by norm_num [Nat.gcd]
_ = Nat.gcd 10 6 := by norm_num [Nat.gcd]
_ = Nat.gcd 6 4 := by norm_num [Nat.gcd]
_ = Nat.gcd 4 2 := by norm_num [Nat.gcd]
_ = 2 := by norm_num [Nat.gcd]No goals
11. Define something when the argument needs it
On paper: “let ”: a name introduced when the argument needs it.
In Lean: the new name receives a type and a definition; its values can be explored, and claims about it stated separately.
Example
Define Euler’s polynomial .
Lean words:
def introduces the name; #eval computes a value; rfl can prove an equality obtained directly from the definition.def eulerPolynomial (n : Nat) : Nat := n^2 + n + 41Definition accepted: eulerPolynomial
Lean accepts
eulerPolynomial as a function from natural numbers to natural numbers. That name is now available below.Are the first forty values, to , all prime?
List.range 40 is the list ; .all tests every element with the function written after fun n =>.#eval (List.range 40).all (fun n => Nat.Prime (eulerPolynomial n))true
Lean answers
true: all forty are prime. #eval computes and displays; it does not prove, and the theorem below is what Lean checks.At , Euler’s polynomial is .
theorem euler_polynomial_40 : eulerPolynomial 40 = 41^2 := by
rflProof checked: euler_polynomial_40
theorem euler_polynomial_40 : eulerPolynomial 40 = 41^2 := by⊢ eulerPolynomial 40 = 41 ^ 2
rfl
No goals
What Lean adds: the theorem records the first composite value after that run. Reduction of the definition proves the exact equality.
Exercise
Define and prove .
Solution
def eulerSeventeen (n : Nat) : Nat := n^2 + n + 17
theorem euler_seventeen_16 : eulerSeventeen 16 = 17^2 := by
rflDefinition accepted: eulerSeventeen
Proof checked: euler_seventeen_16
theorem euler_seventeen_16 : eulerSeventeen 16 = 17^2 := by⊢ eulerSeventeen 16 = 17 ^ 2
rfl
No goals
12. Prove a whole family by induction
On paper: “it holds for 0; if it holds for , it holds for ”: induction.
In Lean: induction separates from the step that carries the result from to .
Example
For every natural , the sum of the first odd numbers is .
Lean words:
induction n with opens the two cases; ih is the result already available for ; Finset.range n is the set and .sum adds the function over it; Finset.sum_range_succ separates the last term of the finite sum; simp closes the case , where the sum is empty.theorem sum_first_odd (n : Nat) :
(Finset.range n).sum (fun k => 2*k + 1) = n^2 := by
induction n with
| zero => simp
| succ n ih =>
rw [Finset.sum_range_succ, ih]
ringProof checked: sum_first_odd
theorem sum_first_odd (n : Nat) :
(Finset.range n).sum (fun k => 2*k + 1) = n^2 := byn : ℕ ⊢ ∑ k ∈ Finset.range n, (2 * k + 1) = n ^ 2
induction n with
| zero => simp
| succ n ih =>
rw [Finset.sum_range_succ, ih]
ringNo goals
What Lean adds: induction produces the case and the step from to . In the step,
ih supplies the sum through ; the final term completes the next square.Exercise
Prove Gauss’s formula by induction.
Solution
theorem gauss_sum (n : Nat) :
2 * (Finset.range (n + 1)).sum (fun k => k) = n * (n + 1) := by
induction n with
| zero => simp
| succ n ih =>
rw [Finset.sum_range_succ]
rw [mul_add, ih]
ringProof checked: gauss_sum
theorem gauss_sum (n : Nat) :
2 * (Finset.range (n + 1)).sum (fun k => k) = n * (n + 1) := byn : ℕ ⊢ 2 * ∑ k ∈ Finset.range (n + 1), k = n * (n + 1)
induction n with
| zero => simp
| succ n ih =>
rw [Finset.sum_range_succ]
rw [mul_add, ih]
ringNo goals
mul_add is the distributive law, , from Mathlib; rewriting with it separates twice the sum through , the left side of ih, which then replaces it.13. Let a CAS explore; let Lean certify
On paper: a computation in the margin suggests an identity; the proof states it and justifies it.
In Lean: a CAS may suggest the polynomial identity. Lean then states its domain and checks a proof independently.
Example
SymPy factors , the expression in that identity.
Lean words: a SymPy input explores the factorization;
theorem states it in Lean; ring proves the identity.factor((m**2 - n**2)**2 + (2*m*n)**2)(m^2 + n^2)^2
SymPy returns . This is a candidate identity; its domain and proof have not yet been supplied.
The candidate, stated for real .
theorem pythagorean_parameterization (m n : ℝ) :
(m^2 - n^2)^2 + (2*m*n)^2 = (m^2 + n^2)^2 := by
ringProof checked: pythagorean_parameterization
theorem pythagorean_parameterization (m n : ℝ) :
(m^2 - n^2)^2 + (2*m*n)^2 = (m^2 + n^2)^2 := bym n : ℝ
⊢ (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2
ring
No goals
What Lean adds: Lean accepts the identity after
ring constructs its proof. The result now belongs to the exact universal statement shown above.A CAS answer can hold only under a condition it does not state. SymPy simplifies to :
cancel((x**2 - 1)/(x - 1))x + 1
As a Lean theorem, the claim needs the condition as a hypothesis; at the two sides differ. With a right-click on the line above, Use as Lean candidate, the Workspace writes the theorem for that answer; the theorem carries that hypothesis.
field_simp clears the denominator, which that hypothesis allows; ring finishes.theorem cancel_with_condition (x : ℝ) (h1 : x - 1 ≠ 0) :
(x^2 - 1) / (x - 1) = x + 1 := by
field_simp
ringProof checked: cancel_with_condition
theorem cancel_with_condition (x : ℝ) (h1 : x - 1 ≠ 0) :
(x^2 - 1) / (x - 1) = x + 1 := byx : ℝ
h1 : x - 1 ≠ 0
⊢ (x ^ 2 - 1) / (x - 1) = x + 1
field_simp
x : ℝ
h1 : x - 1 ≠ 0
⊢ x ^ 2 - 1 = (x - 1) * (x + 1)
ring
No goals
The cancellation holds for every real except 1.
Exercise
Every odd number is a leg of a Pythagorean triple: find integers with .
Solution
theorem odd_leg (k : ℤ) : ∃ b c : ℤ, (2*k + 1)^2 + b^2 = c^2 := by
use 2*k^2 + 2*k, 2*k^2 + 2*k + 1
ringProof checked: odd_leg
theorem odd_leg (k : ℤ) : ∃ b c : ℤ, (2*k + 1)^2 + b^2 = c^2 := byk : ℤ
⊢ ∃ b c, (2 * k + 1) ^ 2 + b ^ 2 = c ^ 2
use 2*k^2 + 2*k, 2*k^2 + 2*k + 1
case h
k : ℤ
⊢ (2 * k + 1) ^ 2 + (2 * k ^ 2 + 2 * k) ^ 2 = (2 * k ^ 2 + 2 * k + 1) ^ 2
ring
No goals
A CAS can suggest and ;
use supplies them, and ring checks the identity for every .What “Proof checked” says
Lean’s kernel, a small checker at its core, checks the proof that the written steps and any tactics produce. This separates discovery from trust: a person, tactic, CAS or AI may suggest the proof, but the suggestion receives no special privilege. The kernel accepts the resulting proof, or it does not. A step that fails says that this proof did not work, not that the claim is false.
The check is relative to the definitions, earlier theorems and axioms on which the result depends.
#print axioms displays the axioms used by a theorem.#print axioms pythagorean_parameterization'pythagorean_parameterization' depends on axioms: [propext, Classical.choice, Quot.sound]
A green result applies to the statement actually shown. After a source input changes, Enter checks it again so that the displayed result belongs to the current source.
The vocabulary you now have
The main flow:
theorem opens a precise claim; goals display what remains; tactics build the proof; the kernel checks it.- Assume, expose and supply:
intro,obtain,exact,apply,have,rcases. - Split and choose:
constructor,left,right. - Transform:
rw,simp. - Inspect and calculate:
#check,#eval,rfl,norm_num,ring. - Arithmetic consequences:
omega,linarith,nlinarith. - Build mathematical forms:
use,calc,induction. - Introduce an object when needed:
def.
That vocabulary is enough to read every proof in this tutorial and to begin translating familiar arguments of your own. When a needed theorem or tactic is unfamiliar, Help ▸ Command help is the dictionary and Mathlib is the library. The goal tells you what kind of move must come next.
Where to continue
A short proof already understood on paper makes a useful next step. Its statement can come first, followed by one mathematical move at a time and the new goal after each. A computation that helps discover the result can remain beside the proof; the result is stated separately and Lean checks it.
Further reading: Theorem Proving in Lean 4 explains Lean, and Mathematics in Lean develops mathematical examples with Mathlib.