using a computer to prove a + b = b + a

succ succ succ succ succ succ succ

In this post I’ll prove the seemingly trivial fact that addition over the natural numbers is commutative. That is, $a + b = b + a, \forall a, b \in \mathbb{N}$ .

The proof will be by the Peano axioms, and it’s structure is actually very simple. To make things more interesting, I’ll be doing the proof using the proof assistant Lean 4.

Peano axioms

The first step is to formalize the Peano axioms for addition in Lean. Using these axioms, we recursively define the natural numbers (including $0$ ):

$0$ is a natural number,
define the successor function $S$ , then for every natural number $n$ , we have $S(n)$ is a natural number.

Informally, $S(n) = n + 1$ for all $n \in \mathbb{N}$ . In Lean, this looks like:

inductive nat where
  | zero : nat
  | succ : nat -> nat

Using this definition of the natural numbers, we can define addition as:

$a + 0 = a$ ,
$a + S(b) = S(a + b)$ .

def add : nat -> nat -> nat
  | a, zero => a
  | a, succ b => succ (add a b)

-- use + symbol
instance : Add nat where
  add := nat.add

first two results

With this, we have our first two results. First, add_zero, a proof of $n + 0 = n, \forall n \in \mathbb{N}$ . This follows by the first part in the definition of addition. We can use the rfl tactic, which stands for reflexivity, to directly prove by definition.

theorem add_zero (n : nat) : n + zero = n := by
  rfl

Next, we have add_succ, a proof of $a + S(b) = S(a + b), \forall a, b \in \mathbb{N}$ . Similar to above, this follows by the second part of our definition of addition. Once again we use the rfl tactic.

theorem add_succ (a b : nat) : a + succ b = succ (a + b) := by
  rfl

towards commutativity

A good step towards commutativity would be to prove commutativity of addition with zero first. That is, zero_add, a proof of $0 + n = n, \forall n \in \mathbb{N}$ . Note that this is not directly given by our definitions, so we have to do a bit more work for it. We will use induction on $n$ , so let’s tell Lean about this plan. Note that the sorry tactic magically proves anything, but does not count as a formal proof. It’s simply there to prevent Lean from complaining about syntax errors.

theorem zero_add (n : nat) : zero + n = n := by
  induction n with
  | zero => sorry
  | succ n ih => sorry

We’ve split the proof into two cases: the base case and the induction step. The base case is when $n = 0$ , indicated by the | zero pattern match. Here our goal is $\empty \vdash \text{zero} + \text{zero} = \text{zero}$ . Let’s rewrite the left hand side to just $0$ using add_zero:

theorem zero_add (n : nat) : zero + n = n := by
  induction n with
  | zero => rw [add_zero]
  | succ n ih => sorry

At this point, we’ve reduced the goal to $\empty \vdash \text{zero} = \text{zero}$ , which Lean is smart enough to figure out is true. Let’s move on to the induction step. Here, we pattern match | succ n ih, where ih is the induction hypothesis, or a proof of $\text{zero} + n = \text{zero}$ . Our goal is $\text{ih} \vdash \text{zero} + \text{succ n} = \text{succ n}$ . We can rewrite the left hand side with add_succ to get succ (zero + n), then rewrite with ih to get succ n, equating the right hand side and thus finishing the proof.

theorem zero_add (n : nat) : zero + n = n := by
  induction n with
  | zero => rw [add_zero]
  | succ n ih => rw [add_succ, ih]

In a similar way, we prove succ_add, that $S(a) + b = S(a + b), \forall a, b \in \mathbb{N}$ . For this, we use induction on $b$ .

The base case is succ a + 0 = succ (a + 0). First rewrite with add_zero to succ a = succ (a + 0), then rewrite again with add_zero to succ a = succ a.
For the induction step we have ih: succ a + b = succ (a + b) and we wish to prove succ a + succ b = succ (a + succ b). First rewrite with add_succ to get succ (succ a + b) = succ (a + succ b), then with ih to get succ (succ (a + b)) = succ (a + succ b), and finally with add_succ again to get succ (succ (a + b)) = succ (succ (a + b)).

theorem succ_add (a b : nat) : succ a + b = succ (a + b) := by
  induction b with
  | zero => repeat rw [add_zero]
  | succ b ih => rw [add_succ, ih, add_succ]

putting it all together

Finally, we have all the ingredients needed to prove $a + b = b + a, \forall a, b \in \mathbb{N}$ . This will be done by induction on $b$ . I will not go into as much detail this time, the proof looks like:

theorem add_comm (a b : nat) : a + b = b + a := by
  induction b with
  | zero =>
    rw [zero_add]
    rfl
  | succ b ih =>
    rw [add_succ, ih, succ_add]

The full Lean file is available here.

why all this work?

I’ve been meaning to teach myself Lean for a while now, but never found the time to get around to it. This language is definitely the most prerequisite heavy one I’ve looked at to date. Not only do I need to know the basics of mathematical proofs, but also some first-order logic to be able to undestand what the assistant is telling me, and also why the prover works.

Writing this was my excuse to finally dip my toes in the world of computer assisted proofs. I’ve always thought of mathematical proofs as a form of art, as there typically isn’t an algorithmic way to go about them. But having seen Lean, although it can’t (yet) write an entire proof by itself, it amazes me to see a computer program be able to validate a proof. I will definitely be spending more time with this language in my future studies.