Beyond Booleans

What a logical statement really is

In TypeScript—and in most programming languages—an expression like 2 + 2 = 4 is a Boolean. The language immediately collapses it into either true or false, and the type of the whole expression is just boolean. You can write type annotations, but they’re redundant:

There is exactly one boolean type, and it has exactly two values. That model works well for computation, but it hides something important: the knowledge of which facts have actually been established.

The Lean theorem prover takes a different approach. In Lean, a statement like 2 + 2 = 4 does not evaluate to a verdict. Instead, the expression itself is a value of a type called Prop—short for "logical proposition":

Lean will happily tell you that 2 + 2 = 4 is a proposition, but it will not tell you whether it’s true. To establish truth, you must construct a proof.

Propositions as types

Here is the key twist: in Lean, a proposition like 2 = 2 is not only a value of type Prop; it is also itself a type. A proof is a value of that type:

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

The by rfl in the proof is a tactic that constructs a value of type claim1, i.e., a value of type 2 = 2. We could equally write the proposition directly as the type:

def proof1 : 2 = 2 := by rfl

So we have a "type tower": the value by rfl has type 2 = 2, and 2 = 2 has type Prop. Nothing like this exists in TypeScript, but in Lean it is routine.

Proving a proposition means producing a value of its type. Verifying a mathematical claim is nothing more than typechecking. If you can construct a well-typed value of type 2 + 2 = 4, you have proven it:

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

But what about false claims? If you try to write by rfl for a proposition like 2 + 2 = 5, the type checker rejects it. There is no way to produce a value of that type without cheating (using sorry or a bad axiom):

That alone doesn’t prove 2 + 2 = 5 is false—maybe we just haven’t found a proof yet. To actually state falsehood, we prove the negation:

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

Note the Not in front: Not (2 + 2 = 5) is itself a proposition, and by decide generates a proof of it. Since the expression typechecks, Lean has verified that 2 + 2 = 5 is false. In this sense, a false proposition is like the never type in TypeScript: a type no one can inhabit without cheating.

Proofs are interchangeable

A proposition may have zero proofs or infinitely many. For example, 2 + 2 = 4 can be proven with by rfl, with by decide, or by referring to the Mathlib theorem two_add_two_eq_four:

import Mathlib
 
def proof2 : 2 + 2 = 4 := by rfl
def proof2' : 2 + 2 = 4 := two_add_two_eq_four
def proof2'' : 2 + 2 = 4 := by decide

All of those values have the same type. Lean enforces proof irrelevance: once a proof typechecks, every proof of the same proposition is indistinguishable from any other. A proposition therefore has at most one "distinct" proof. If you have one, the proposition is true; if the negation is provable, it is false.

Typed truth

Why does any of this matter outside pure mathematics? It enables what you might call typed truthfulness: facts can be attached to data as types, and the compiler enforces them.

Suppose you need a function that only accepts a number strictly between 0 and 1. In TypeScript, you can’t express that constraint in the type system—not much beyond throwing a runtime error:

function someFunction(x: number) {
  if (x >= 0 && x <= 1) {
    return x ** 2;
  } else {
    throw RangeError('x must be between 0 and 1');
  }
}

In Lean, the constraint is trivial. The function takes a real number x, plus two proofs—one that x ≥ 0 and one that x ≤ 1:

def someFunction (x: ℝ) (x_ge_zero: x ≥ 0) (x_le_one: x ≤ 1) :=
  x ^ 2

Callers must supply those proofs. For literals like 0.99, the tactic by norm_num handles it. For values outside the range, the typechecker fails:

Lean gives you a way to pass facts around the program as first-class values, and to be certain they hold wherever they are used.

Nor are you limited to concrete literals. The same machinery composes proofs about arbitrary expressions. Suppose you’re working with x = (sin a) ^ 2 and you need to pass x to someFunction. You cannot compute the value of sin a, but you can prove its square is between 0 and 1 using Mathlib’s existing theorems:

noncomputable def someOtherFunction (a: ℝ) :=
  let x := (Real.sin a) ^ 2
  have x_ge_zero := by apply sq_nonneg
  have x_le_one := by apply sin_sq_le_one
  someFunction x x_ge_zero x_le_one

Lean’s interactive apply? search finds sq_nonneg (for the lower bound) and sin_sq_le_one (for the upper bound). The proofs then typecheck even though Real.sin itself is noncomputable—mathematics routinely deals with objects like the sine of a real number, which cannot be reliably computed with finite precision. Lean proves facts about them anyway by composing proofs, not by computation.

What a proof actually is

So what does by rfl produce? Under the hood, 2 = 2 is syntax sugar for Eq 2 2, where Eq is a type defined in Lean’s core library:

inductive Eq : α → α → Prop where
  /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
  equality type. See also `rfl`, which is usually used instead. -/
  | refl (a : α) : Eq a a

The definition of Eq is a hybrid between a function and a type. Its only constructor, Eq.refl, produces a value of type Eq x x for any x. You can get Eq.refl 2 of type Eq 2 2, but it is impossible to construct a value of type Eq 2 3.

That impossibility is precisely what it means for 2 = 3 to be unprovable. The claim "you cannot construct a value of type Eq 2 3" is the same as "you cannot prove 2 = 3." Types thereby express mathematical truth (this is known as the Curry–Howard correspondence).

The by rfl tactic is just a small piece of the puzzle. It generates a proof term:

def claim1 : Prop := 2 = 2    /- or := Eq 2 2 -/
def proof1 : claim1 := by rfl /- or := Eq.refl 2 -/

Once the term Eq.refl 2 is constructed, the kernel—Lean’s tiny typechecking core—verifies the types. If the proof typechecks, the argument must be correct. Compose these terms, and you can build and verify entire mathematical theories, all as ordinary typechecking. It turns out that even Or, And, and Not can be defined in terms of types of proofs and functions between them—logic itself becomes a programming language.