A Fairly Aimless Post About Using Lean for Math

A hardware person finally uses a proof assistant for math. Also some pontificating on CS education, kind of.

I am in a class on formalizing mathematics this semester¹. One of the readings was Patrick Massot’s essay on “Why Formalize Math?”, and one reason he gives was teaching undergraduate students about mathematics using a theorem prover. To paraphrase the argument, using an interactive theorem prover forces a certain level of specificity when writing down theorems, and has a well-defined language to precisely articulate what students are trying to prove, coupled with the actual machinery to be able to check those proofs for accuracy.

So for fun (and to improve my own skills with theorem provers), I set out to try to redo some of my discrete math homeworks from spring 2021² in Lean.

The first theorem that we are asked to prove is:

$$(\forall q \in ℚ)[(3q^2 - 2q + 4) \in ℚ]$$

The sketch of this proof is that we can introduce a ratio of integers $r, k$ to represent $q$ (assuming $k \neq 0$). From here, we can manipulate the expression using normal arithmetic rules to get a single ratio of multiples of $r$ and $k$. Any rational number can be represented as the ratio of integers, and the new form of the expression is exactly in line with this definition, so we have a rational number. QED.

As far as I could tell, there was no way in Mathlib (Lean’s math formalization library) to specifically ask whether something is a rational number³. The best that could be done was kind of a workaround (asking whether for a given real number, there exists a rational number equal to its value):

def IsRational (x : ℝ) : Prop :=
  ∃ q : ℚ, (q : ℝ) = x

Next, I defined the quadratic expression that we’re asked to prove as a function. I am pretty sure there is a way to do this inline with the theorem declaration, but I ended up just going with this:

def expr (x : ℚ) : ℝ :=
  3 * (x : ℝ)^2 - 2 * (x : ℝ) + (5/7 : ℚ)

To set up the proof, we need to introduce two (integer) variables:

variable (r : ℤ)
variable (k : ℤ)

We can now state the actual theorem as:

theorem q1 (x : ℚ) {hh: k ≠ 0} {h: x = r / k} : IsRational (expr x)

To break this down a bit further, we want to prove that the result of expr x is rational for any rational input $x$. As part of the proof, we introduce two integers (previously declared), where the ratio of the two represents $x$ (part of the definition of a rational number is that it can be represented as the ratio of integers). We also guarantee that $k$ is nonzero to prevent divide-by-zero problems in the proof.

After the theorem declaration, we switch into proof mode:

theorem q1 (x : ℚ) {hh: k ≠ 0} {h: x = r / k} : IsRational (expr x) := by
  unfold expr
  unfold IsRational
  rw [h]
  rw [@pow_two]
  norm_cast
  simp

The unfold tactics substitute the function bodies in for the invocations given in the theorem definition. Then we can rw (rewrite) the goal state using the ratio definition for $x$ that we introduced in the theorem definition ($x = \frac{r}{k}$). We are now given the goal state:

∃ q, ↑q = 3 * ↑(↑r / ↑k) ^ 2 - 2 * ↑(↑r / ↑k) + ↑(5 / 7)

where the “↑” denotes coercing the variable type to match what we want⁴. This means that we are now trying to prove that there is a rational number $q$ whose value is the same as the (type-coerced) result of evaluating $3(\frac{r}{k})^2 - 2\frac{r}{k} + \frac{5}{7}$, i.e. that the expression’s output could be represented as a rational number.

I’ve now reached the part where I get a bit frustrated with Lean potentially oversimplifying things. I call a theorem from Mathlib (pow_two), which allows me to rewrite the $\frac{r}{k}$ ratio as $\frac{r}{k}*\frac{r}{k}$. I follow that up with the norm_cast tactic, which (as far as I understand, and this may be wrong), resolves the type conversions and introduces Mathlib’s definition of dividing integers from its Rat (rationals) library. Finally, one final simp invocation (presumably) uses the Mathlib definitions of integer division to resolve the proof.

There are probably better ways to prove this in a way that feels more satisfying and less like I am invoking black box theorems and tactics that I don’t actually understand. I’m trying do that with the other problems from this homework - less reliance on black box tactics and trying to get them to align more with my paper proofs/solutions (though admittedly I’ve proven another theorem in this homework using ring, which seems against this spirit).

Altogether, I think this presents a slightly more satisfying use-case of Lean than a lot of the proofs I was trying to do over big-step semantics in my formal methods class last year or at SSFT 2024. After getting through a few more old homework problems, I’ll try to revisit using Lean (or Rocq) for PL/verification work.

With respect to Massot’s essay, I think using theorem provers is probably best reserved for upper undergraduate classes at the least, and should not be used for introductory logic or discrete math classes. While the claim “In such a [structured] proof, levels can be folded and unfolded at will”⁵ is technically true, for Lean/theorem prover novices (like myself) I still don’t think it’s particularly easy to figure out what exactly the tactics are doing without sufficient background about the system itself⁶. As such, I think using theorem provers ends up being more confusing (with respect to getting the right syntax to define theorems) and obscuring proof details (with tactics). I still think paper proofs (with a clearly defined notation for the class) are better in such cases. ⁷

The code is available here.