Each worksheet prints cleanly on A4 or Letter. Answer keys are on a separate page.

The Lumenary · Grades 9–12

First steps in Lean

Name: ______________________

Date: ______________________

You will learn to

Write and check short Lean proofs of propositional tautologies and simple equalities using rfl, intro, exact, constructor, cases, rw and simp
Explain the idea "propositions are types, proofs are terms", for example why a proof of $p \to q$ is a function
Prove a statement about natural numbers by induction in Lean, and explain why $n + 0 = n$ holds by definition while $0 + n = n$ needs induction
Read a Mathlib theorem statement, and distinguish applying a library theorem from proving a result independently
Explain what a machine check guarantees (and what it does not), including sorry, axioms, and mis-stated theorems

1.
Let n : ℕ be a variable. Which of these goals can be closed by rfl alone? (Choose all that apply.)
- A.n + 0 = n
- B.2 + 3 = 5
- C.0 + n = n
- D.n + 1 = 1 + n
2.
A classmate's Lean file compiles with the warning "declaration uses sorry". What can you conclude?
- A.The theorem is not proved: sorry is a placeholder Lean accepts on trust, and #print axioms would list sorryAx.
- B.The theorem is proved, because the file compiles.
- C.The theorem is false.
- D.Lean found a proof automatically and is warning that it is long.
3.
In Lean, what is the value of (7 : ℕ) - 10?
4.
In Lean, what is the value of (17 : ℕ) / 5?
5.
You are proving theorem t (p q : Prop) : p → (q → p) := by and you type intro hp. What does the goal state look like now?
- A.Hypotheses p q : Prop and hp : p; goal ⊢ q → p
- B.Hypotheses p q : Prop and hp : p → q; goal ⊢ p
- C.Hypotheses p q : Prop; goal ⊢ p
- D.No goals: the proof is complete.
6.
Which term is a proof of p ∧ q → q ∧ p?
- A.fun ⟨hp, hq⟩ => ⟨hq, hp⟩
- B.fun ⟨hp, hq⟩ => ⟨hp, hq⟩
- C.fun h => h
- D.⟨hq, hp⟩
7.
The theorem no_nat_sqrt_two : ¬ ∃ q : ℕ, q * q = 2 is proved in Lean without sorry. Does it show that $\sqrt 2$ is irrational?
- A.No. It only says no natural number squares to $2$ ; irrationality is about fractions, which this statement never mentions.
- B.Yes, because Lean checked it.
- C.Yes, because every rational number is a natural number.
- D.No, because the proof must be wrong.
8.
Mathlib contains theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p. Which reading is correct?
- A.For every natural number $n$ there is a prime $p$ with $p \ge n$ .
- B.There is a prime $p$ that is at least as big as every natural number $n$ .
- C.Every natural number $p \ge n$ is prime.
- D.There are exactly $n$ primes.
9.
In the induction proof of 0 + n = n, the inductive step has hypothesis ih : 0 + k = k and goal ⊢ 0 + (k + 1) = k + 1. Which tactic line closes the goal?
- A.rw [Nat.add_succ, ih]
- B.rw [ih]
- C.rfl
- D.exact ih
10.
Truth tables decide propositional tautologies by brute force. Write is_tautology(formula, n), where formula is a Python function of n Booleans, returning True exactly when it is true for all $2^n$ assignments. (In Python, p <= q on Booleans means $p \to q$ .)
Computational — Practice

Answer key — First steps in Lean

1.
n + 0 = n (a defining rule) and 2 + 3 = 5 (a computation with numbers) are closed by rfl. 0 + n = n and n + 1 = 1 + n are true but need proofs — by induction, or by applying Nat.zero_add and Nat.add_comm.
2.
sorry closes any goal without proof. The file compiles with a warning, and the declaration depends on the axiom sorryAx. So nothing has been proved about that statement — it might even be false.
3.
(7 : ℕ) - 10 = 0: truncated subtraction. So a formal statement such as ∀ n : ℕ, n - 1 + 1 = n is false (at $n = 0$ the left side is $1$ ). To talk about $-3$ you would use the integers: (7 : ℤ) - 10 = -3.
4.
(17 : ℕ) / 5 = 3, the quotient of $17 = 5 \cdot 3 + 2$ , and 17 % 5 = 2. For the real number $3.4$ you would write (17 : ℝ) / 5.
5.
After intro hp the state is
```
p q : Prop
hp : p
⊢ q → p
```
Then intro hq gives the goal ⊢ p, and exact hp finishes. As a term, the whole proof is fun hp hq => hp.
6.
fun ⟨hp, hq⟩ => ⟨hq, hp⟩: it receives a proof of p ∧ q, unpacks it into hp : p and hq : q, and builds the pair ⟨hq, hp⟩ : q ∧ p. This is the lesson's and_swap.
7.
" $\sqrt 2$ is irrational" means there are no integers $a, b$ with $b \ne 0$ and $(a/b)^2 = 2$ . The Lean theorem only rules out natural numbers $q$ with $q^2 = 2$ — a much easier fact. A machine-checked proof is only as meaningful as its formal statement.
8.
For every $n$ there exists $p$ with $n \le p$ and $p$ prime: primes exist beyond any bound, which is Euclid's theorem. Swapping the order of the quantifiers would give a false statement — a classic trap in reading formal statements, and in reading quantifiers generally.
9.
rw [Nat.add_succ, ih]. This mirrors the human proof: $0 + (k + 1) = (0 + k) + 1$ by the definition of addition, $= k + 1$ by the induction hypothesis. Together with the base case rfl, this is zero_add_induction.
10.
```
from itertools import product


def is_tautology(formula, n):
    return all(formula(*values) for values in product([True, False], repeat=n))
```
For propositional logic this brute force is a complete decision method (with $2^n$ rows). It checks classical truth: it says ¬¬p → p is a tautology, which Lean proves only with the classical axiom, as the lesson's double_negation shows. For statements about infinitely many numbers, such as $0 + n = n$ , no table can be finished — that is where proofs, and proof assistants, come in.