the lean theorem prover is a pretty cool thing.

---

doing mathematics on the computer is slow and hard. it’s not going to replace doing mathematics by hand, LLMs are not going to replace mathematicians, and mathematics verified on a machine is not inherently “more rigorous” than mathematics verified by humans.

it seems important to preface this post with these observations, because fundamentally this post is about comparing traditional mathematics with using a theorem prover like lean. however, it’s primarily about comparing the experience of doing each of these things, and not their merits. with that out of the way, let’s talk about lean.

suppose we want to show the following is true for natural numbers a and b:

(a+b)^2 = a^2 + 2ab + b^2

a proof of this on paper would look something like this:

(a+b)^2 = (a+b) * (a+b) 
        = (a+b) * a + (a+b) * b
        = a*a + b*a + a*b + b*b
        = a^2 + 2*a*b + b^2

on the other hand, a proof of this in lean looks something like this:

open Nat

example (a b : Nat) : (a+b)^2 = a^2 + 2*a*b + b^2 := by
  repeat rw [pow_two]
  rw [left_distrib, right_distrib, right_distrib, mul_comm b a, mul_assoc, two_mul]
  repeat rw [add_assoc]

it isn’t important to understand the above lean code. what is important is to note the difference between the data provided in each of these. the process of doing the manipulation in lean is method explicit, manipulation implicit: to use rw (the “rewrite” tactic) to modify the goal, we provide the lemma to apply and lean finds where to apply it to the current goal, transforming the goal. the paper proof has this reversed: each state along the way is explicitly written out, but nowhere in the paper proof is it written “by the commutativity of multiplication.” that part of the proof is implicit.

of course, this isn’t a representative example of pen and paper math; often in math papers it is necessary to interrupt calculations with explicit justifications of each step. however, this example serves to highlight a key difference between the kinds of things generally expected to be explicit when doing mathematics in these two different settings, and this difference has a concrete impact on the way that mathematics is conceptualized in these different environments.

many lean users report that the way that they engage with doing proofs in lean is “reactive” in that they are often attempting to simplify the current goal step-by-step rather than planning out a route for their proof. this can lead to proofs in lean being particularly confusing or frustrating to follow. on the other hand, a common complaint about pen and paper mathematics is that justification for steps can often be omitted, usually because those steps are considered “trivial” to the author; since this notion of “trivial” is incredibly subjective, this often leads to its own frustrations for those with different backgrounds. these issues with both forms of mathematics seem to be natural consequences of their formats, and what data is explicit vs. implicit.

---

bonus: it was mentioned above that the pen and paper example was not representative, but neither is the lean example. it was only written like that for illustration; in practice, the same proof can be done as

example (a b : Nat) : (a+b)^2 = a^2 + 2*a*b + b^2 := by linarith

in fact, tactics in theorem provers can be quite sophisticated!

---