Beyond Booleans

What is the type of 2 + 2 = 4?

Beyond Booleans

August 16, 2025

Pay what you like

What is the type of 2 + 2 = 4?

In TypeScript and most other languages, logical expressions have a Boolean type:

const question1 : boolean = 2 === 2; // true
const question2 : boolean = 2 + 2 === 4; // true
const question3 : boolean = 2 + 2 === 5; // false

In fact, we can drop the : boolean type annotations because TypeScript can see that all of these are logical expressions—and so they obviously must be booleans:

[Hover in TypeScript playground: question2 is a boolean]

Note that question1, question2, and question3 are all of the same type. In TypeScript, there is only one boolean type, and only two values (true and false) of that type. Let’s visualize that (an arrow means “a value is of type”):

That’s how logical statements work in the vast majority of programming languages: one type, two values. However, that’s not what happens in Lean.

Propositions as Values

Although Lean can do Booleans, by default it won’t see 2 + 2 = 4 as a Boolean. Instead, 2 + 2 = 4 in Lean will give you a Prop—short for “logical proposition”:

[Hover in Lean playground showing question2 is of type Prop]

*(Try it in the Lean playground or VS Code.)*

Let’s annotate them explicitly so we remember that 2 + 2 = 4 is of type Prop:

def question1 : Prop := 2 = 2
def question2 : Prop := 2 + 2 = 4
def question3 : Prop := 2 + 2 = 5

Now let’s visualize these values and types (an arrow means “is a value of type”):

This looks different!

When you write 2 + 2 === 4 in TypeScript, it immediately “collapses” into some boolean (with a possible value of true or false—in this case, it’s true).

But when you write 2 + 2 = 4 in Lean, it doesn’t “collapse” into a verdict. The logical statement itself is a distinct value. It doesn’t “turn” into a true or a false. A proposition remains a proposition—a speculative claim; a logical sentence.

So how do you know if a proposition is true?

You compute it!

Just kidding.

In Lean, you must convince the computer it’s true—by presenting a proof. Turns out, not only is 2 + 2 = 4 a value, it is also a type. A proof is a value of that type.

Let’s unpack this.

Propositions as Types

Consider this proposition:

def claim1 : Prop := 2 = 2

How can you convince a computer that 2 = 2 is true? Your programmer instinct might be to just calculate both sides and compare them, but Lean is primarily used by mathematicians, and mathematics strays far outside the realm of computation. For example, if you tried to “compute both sides” to prove that 1 + 1/2 + 1/4 + 1/8 + ... = 2, your program would require infinite time and infinite memory.

Instead, Lean forces you to think like a mathematician. To prove a claim, you need to supply a proof that builds on axioms and other proofs and connects them into a logical argument. If you’ve managed to construct a proof, you’ve proven the claim.

Let us supply a proof for this claim:

def claim1 : Prop := 2 = 2
def proof1 : claim1 := by rfl

(Try it in the Lean playground.)

For now, don’t worry about what by rfl really means; we’ll get to that a bit later. Think of it as a built-in Lean value that can prove any statement like foo = foo.

However, look at the types! Like in the earlier example, 2 = 2 is of type Prop. But here’s something strange: by rfl itself is of type claim1 (which is 2 = 2).

In fact, we could replace : claim1 with : 2 = 2 and it would still typecheck:

def proof1 : 2 = 2 := by rfl

This means that our proposition 2 = 2 is not only a value, but it can also act as a type (and by rfl here happens to produce a value of exactly the 2 = 2 type):

You can’t have such a “type tower” in TypeScript, but in Lean this is absolutely fine. The by rfl value has a type of 2 = 2, and 2 = 2 has a type of Prop.

Now, here’s what this means.

The fact that we were able to produce some value of the type 2 = 2 means that we have proven it. Proving a proposition means producing a value of its type. Verifying any mathematical result in Lean is nothing more than typechecking.

Since you’ve managed to produce a value of type 2 = 2 and 2 + 2 = 4 (either of these can be done with by rfl), you have effectively proven these propositions:

def proof1 : 2 = 2 := by rfl
def proof2 : 2 + 2 = 4 := by rfl

However, no matter how hard you try, unless there’s a bug in Lean kernel, you can’t produce a value of type 2 + 2 = 5 without either a sorry or a bad axiom:

[Screenshot of linked playground]

*(Try it in the Lean playground.)*

Let’s visualize the fact that we found some proofs for 2 = 2 and 2 + 2 = 4:

Unlike 2 = 2 and 2 + 2 = 4, the 2 + 2 = 5 type is “lonely”—we haven’t found any proof for it. Is that what it means for a proposition to be false?

A careful reader might note that we haven’t actually proven that 2 + 2 = 5 is false. What if it’s true, and we just weren’t lucky enough to produce a proof of it?

In other words, what if 2 + 2 = 5 is unprovably true?

Note the Not

This is an entirely valid concern!

One thing we could do is to look for a proof of the negation of our proposition:

def proof1 : 2 = 2 := by rfl
def proof2 : 2 + 2 = 4 := by rfl
def proof3 : Not (2 + 2 = 5) := by decide

*(Try it in the Lean playground.)*

Note the Not in front of 2 + 2 = 5. You can think of Not (2 + 2 = 5) as a whole separate proposition, and we’ve just supplied a proof for it (by decide):

It typechecks, therefore we know that Not (2 + 2 = 5) is true.

You might be wondering what by decide does. Previously, we’ve only used by rfl—but it can only ever produce proofs of types like foo = foo (e.g. 2 = 2). The reason by rfl could solve 2 + 2 = 4 is because 2 + 2 and 4 unfold into Nat.zero.succ.succ.succ.succ on both sides by definitions of 2, +, and 4. So even 2 + 2 = 4 is actually shaped like foo = foo, which works for by rfl.

However, by rfl can’t produce a proof of a proposition shaped like Not (foo = bar). This is why we had to use the more powerful by decide, which generates a proof of any computable statement. It’s like pulling out a calculator in the middle of a math proof. Although it is possible to prove 2 + 2 is not 5 step-by-step with “mindless” logical transformations, it’s tedious so by decide does this for us.

The important part is that it typechecks. Both by rfl and by decide merely generate proofs (we’ll see what proofs are a bit later), but the tiny Lean kernel does the actual typechecking. If the proof typechecks, the argument must be correct.

[...]

Original source