When I started at the university, I was supposed to study physics. However, what I soon realized was that I felt a special affinity for pure math. It’s not that easy to explain. All I know is that there is something special about definitions and proofs. The way they build on each other and cut through seemingly impossible terrain is a miracle that is not really easy to explain. Rather, it has to be seen firsthand.

So, I worked. I wanted to understand these proofs. I wanted to be able to write them on my own and maybe even invent new ones.

After a lot of hard work, I became somewhat fluent in them. You could say I got used to them. I could even perform tasks that go beyond mere mechanical repetition of previously read material. I could understand why an argument works, and I could understand why it fails. Still, — echoing von Neumann — even though I had gotten used to mathematical proofs, I felt I didn’t quite get them somehow.

Then I learned Lean.

If the first turning point of my mathematical education was to become fluent in proofs, the second one was actually understanding them through Lean. In this post I’ll do what can be done in a very limited space to share this insight.

A syllogism

Viewed from afar, proofs are simple: You introduce assumptions, then you explain why these assumptions produce a conclusion.

Here’s a well-known syllogism:

1. All men are mortal.
2. Socrates is a man.
3. Therefore, Socrates is mortal.

It’s evident that the combination of 1 and 2 implies 3. A proof boils down to noticing that, given that Socrates is a man, assumption 1 means, in particular, that he is also mortal, and this is exactly what is claimed in 3.

This simple example encompasses essentially what deductive reasoning is. The thing is that, while “real” mathematics is exactly like this on some level — it’s always a game of assumptions yielding conclusions — it gets more difficult. As things become more abstract and subtle, a need for heavier machinery emerges. Specifically, we need to express our claims and reasoning in terms of symbolic logic.

A formalised syllogism

Consider the assumption “all men are mortal”. Denoting the set of all men by $A$, and the set of all mortal beings by $B$, this is essentially an inclusion: If an entity is a man, i.e. the entity is an element of the set $A$, then our assumption implies that it’s also $B$ (i.e. a mortal being). Thus, expressed in terms of sets, the assumption “all men are mortal” is $A \subseteq B$.

Now, consider the assumption “Socrates is a man”. Denoting “Socrates” by $x$, and using our previously defined set $A$, the assumption “Socrates is a man” simply translates to $x$ being an element of $A$, i.e $x \in A$.

Now we need to combine our assumptions $A \subseteq B$ and $x \in A$. In logic, this is the “and” operator $\land$. So, in order to express a single assumption which reads “all men are mortal, and Socrates is a man", we write $A \subseteq B \land x \in A$

Finally, we want to express the whole thing: $$ A \subseteq B \land x \in A \Rightarrow x \in B.$$ Notice the implication $\Rightarrow$. On the left we have the symbolic expression that translates to “all men are mortal, and Socrates is a man". On the right we have $x \in B$. As $B$ denotes the set of mortal beings, this is the original syllogism in a symbolic form.

Theorems as types

Now that we have expressed our syllogism in a symbolic form: $$ A \subseteq B \land x \in A \Rightarrow x \in B,$$ we may ask what this statement really is.

It is a sequence of symbols that we have assigned a meaning in terms of natural language, yes, but that doesn’t really give us much. Specifically, considering this implication as a mere sequence of symbols does not give any indication of how it should be treated in a way that would be tractable for computers.

How Lean tackles this is a Curry-Howard-flavoured approach. Specifically, logical statements are treated as types.

In Lean, there are familiar types such as numbers and strings. The type system of Lean is, however, much more flexible than people are usually accustomed to. Something as wild as $$ A \subseteq B \land x \in A \Rightarrow x \in B$$ can be a perfectly valid type in Lean.

Written in Lean, the mortality of Socrates is almost the same as above. The type that corresponds to that specific proposition is

A ⊆ B ∧ x ∈ A → x ∈ B

In order to express this properly, we need some boilerplate:

import Mathlib.Data.Set.Basic

variable {α : Type} {A B : Set α} {x : α}

theorem socrates_is_mortal {α : Type} {A B : Set α} {x : α} :
A ⊆ B ∧ x ∈ A → x ∈ B := by
intro ⟨h1, h2⟩
exact h1 h2

Let’s break this down. The significant bit is this:

theorem socrates_is_mortal {α : Type} {A B : Set α} {x : α} :
A ⊆ B ∧ x ∈ A → x ∈ B := by
intro ⟨h1, h2⟩
exact h1 h2

In general, Lean follows this syntax

theorem name : signature := proof

So we have a theorem socrates_is_mortal. What we want to prove, i.e. the logical proposition A ⊆ B ∧ x ∈ A → x ∈ B, is a type within the signature. Finally, the proof (a term) is the following sequence of symbols:

by
intro ⟨h1, h2⟩
exact h1 h2

This post is not a Lean tutorial, and I’m not going to explain the true meaning of this term. It essentially translates to "clearly" or "just unfold the definitions". What I would like to do instead is to highlight what actually happened here.

In Lean, a proof amounts to building a type. If we want to show that A ⊆ B ∧ x ∈ A → x ∈ B is a true proposition, we need to show that the corresponding type is non-empty, i.e. it can be built from the assumptions and existing results. This kind of construction is something that a computer can verify, so it’s correct with absolute certainty.

Also, we can never prove a false result. If we consider a type corresponding to a false claim, such as 1 = 0, there is no corresponding term. In other words, a claim is true exactly when the corresponding type can be derived from what already exists.

So this term

by
intro ⟨h1, h2⟩
exact h1 h2

tells Lean how to construct our goal type. Since such construction exists and is valid, the fact that Socrates is indeed mortal has now been verified with an absolute certainty.

Conclusion

What I really wanted to highlight in this post is the shift in thinking that occurs under Lean. Theorems and their proofs become something so tractable that even a computer can understand them. They are types and terms. There is no magic. No interpretation. A proof is a mere application of existing terms against each other.

I don’t think this is a very natural way for most people to think about mathematics. Still, for me, it made something click. It acts as a kind of a grounding mechanism: When things get highly abstract it helps to keep in mind that, at the end of the day, they are something that even a computer incapable of any creativity or imagination can understand.