Factorials, binomial coefficients, and Fibonacci numbers in Lean

This tutorial assumes no prior experience with Lean. It alternates short explanations with exercises, and it uses only core Lean, without Mathlib.

Everything runs in the browser at live.lean-lang.org. Each link opens a new tab. Close the previous tab when you open the next exercise, to avoid overloading the server. Each exercise file starts with the solutions to the earlier ones. The editor keeps your code in the address bar, so to save your work, bookmark the page or copy the address.

Session 1: Define, compute, conjecture

Recursion

0! = 1, \qquad (n+1)! = (n+1) \cdot n!

A recursive definition gives the value at $n + 1$ in terms of the value at $n.$ The base case is 0.

Lean

def fact : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * fact n

#eval fact 5 computes a value.
example : fact 5 = 120 := by rfl states a fact, and Lean checks it.

Open demo in Lean

Exercise 1: Factorial and sums

Prove fact 6 = 720 two ways, complete sumTo, and add up odd numbers.

Open Exercise 1 in Lean

Binomial coefficients

$C(n, k)$ is the number of ways to choose $k$ items from a collection of $n.$

\begin{aligned} C(n, 0) &= 1 \\ C(0, k+1) &= 0 \\ C(n+1, k+1) &= C(n, k) + C(n, k+1) \end{aligned}

Pascal's rule. To choose $k + 1$ items from $n + 1,$ consider the first one. Either we choose it, and then we choose $k$ more from the other $n,$ or we don't, and we choose all $k + 1$ from the other $n.$

            1
          1   1
        1   2   1
      1   3   3   1
    1   4   6   4   1
  1   5  10  10   5   1

Lean

def choose : Nat → Nat → Nat
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => choose n k + choose n (k + 1)

Fibonacci numbers have two base cases.

F_0 = 0, \qquad F_1 = 1, \qquad F_{n+2} = F_n + F_{n+1}

0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, \ldots

Open demo in Lean

Exercise 2: Experiments

Print Pascal's triangle, compute, and write down conjectures.

Open Exercise 2 in Lean

Conjectures

Do Exercise 2 before reading this list.

Row sums: $C(n, 0) + \cdots + C(n, n) = 2^n$
$C(n, 1) = n,$ $\; C(n, n) = 1,$ and $C(n, k) = 0$ when $n < k$
$C(n, k) = n! / (k!\,(n-k)!)$
$F_0 + F_1 + \cdots + F_{n-1} + 1 = F_{n+1}$
$1 + 3 + 5 + \cdots + (2n - 1) = n^2$
The shallow diagonals of Pascal's triangle add up to Fibonacci numbers.

Proof by induction

To prove $P(n)$ for every $n$ :

Base case. Prove $P(0).$
Induction step. Assume $P(n)$ (the induction hypothesis) and prove $P(n + 1).$

Example: $1 + 3 + \cdots + (2n - 1) = n^2.$

Base: the empty sum is $0 = 0^2.$
Step: $[1 + 3 + \cdots + (2n - 1)] + (2n + 1) = n^2 + 2n + 1 = (n + 1)^2.$

Lean

theorem sum_odds (n : Nat) : sumTo (fun i => 2 * i + 1) n = n * n := by
  induction n with
  | zero => rfl
  | succ n ih => grind [sumTo]

We set up the induction. The call to grind unfolds sumTo, uses ih, and does the algebra.

Open demo in Lean

Exercise 3: First proofs

Gauss's formula, the sum of Fibonacci numbers, and 0 < fact n.

Open Exercise 3 in Lean

Session 2: Prove

Proofs about `choose`

In the next demo, cases n is similar to induction n, but it splits the proof into cases n = 0 and n = m + 1 without an induction hypothesis. t1 <;> t2 means "do t1, then t2 in every resulting case."

We also need a strengthened version of induction. Suppose the goal is to prove $C(n, k) = 0$ when $n < k.$ Pascal's rule needs the hypothesis for both $k$ and $k + 1.$

induction n: the hypothesis is $P(n, k)$ for this one $k.$ Not enough.
induction n generalizing k: the hypothesis is $P(n, k)$ for every $k.$

Open demo in Lean

Exercise 4: Binomial coefficients

Prove choose n 1 = n and choose n n = 1.

Open Exercise 4 in Lean

A better implementation of the Fibonacci numbers

fib computes the same values over and over:

fib 5
├── fib 3
│   ├── fib 1
│   └── fib 2
│       ├── fib 0
│       └── fib 1
└── fib 4
    ├── fib 2
    │   ├── fib 0
    │   └── fib 1
    └── fib 3
        ├── fib 1
        └── fib 2
            ├── fib 0
            └── fib 1

A faster way: carry two consecutive values along, replacing $(a, b)$ by $(b, a + b)$ at each step.

Lean

def fibLoop : Nat → Nat → Nat → Nat
  | 0, a, _ => a
  | n + 1, a, b => fibLoop n b (a + b)

def fastFib (n : Nat) : Nat := fibLoop n 0 1

steps left	a	b
5	0	1
4	1	1
3	1	2
2	2	3
1	3	5
0	5	8

So fastFib 5 = 5. To prove fastFib n = fib n for all $n,$ we prove something stronger: if the loop starts from $F_m$ and $F_{m+1},$ then after $n$ steps it returns $F_{n+m}.$

Lean

theorem fibLoop_eq (n m : Nat) :
    fibLoop n (fib m) (fib (m + 1)) = fib (n + m)

Open demo in Lean

Exercise 5: Fast Fibonacci is correct

Prove fibLoop_eq, then deduce fastFib n = fib n.

Open Exercise 5 in Lean

The big theorems

Row sums. By Pascal's rule, each entry of row $n$ contributes to exactly two entries of row $n + 1.$ So each row sum is twice the one before, and

C(n, 0) + C(n, 1) + \cdots + C(n, n) = 2^n.

The committee identity. Choose a committee of $k + 1$ from $n + 1$ people, then its chair. Or choose the chair first, then the other $k$ members from the remaining $n.$

C(n+1, k+1) \cdot (k+1) = (n+1) \cdot C(n, k)

The factorial formula, by induction on $n$ :

C(n, k) \cdot k! \cdot (n-k)! = n! \qquad \text{for } k \le n

\begin{aligned} C(n+1, k+1) \cdot (k+1)! \cdot (n-k)! &= C(n+1, k+1) \cdot (k+1) \cdot k! \cdot (n-k)! \\ &= (n+1) \cdot C(n, k) \cdot k! \cdot (n-k)! \\ &= (n+1) \cdot n! \\ &= (n+1)! \end{aligned}

We state it with multiplication because division on Nat rounds down.

Open all the proofs in Lean

Exercise 6: Choose a challenge

Prove the committee identity.
Finish Exercises 4 and 5.
Pascal's diagonals, on paper.
Your own conjecture.

Open Exercise 6 in Lean

Factorials, binomial coefficients, and Fibonacci numbers in Lean

Session 1: Define, compute, conjecture

Recursion

Exercise 1: Factorial and sums

Binomial coefficients

Exercise 2: Experiments

Conjectures

Proof by induction

Exercise 3: First proofs

Session 2: Prove

Proofs about choose

Exercise 4: Binomial coefficients

A better implementation of the Fibonacci numbers

Exercise 5: Fast Fibonacci is correct

The big theorems

Exercise 6: Choose a challenge

Further reading

Proofs about `choose`