Start with a simple question

What is the type of 2 + 2 = 4? In almost every language the answer is boring. Lean answers differently, and the difference changes what a program can promise.

TypeScript collapses the question

Write 2 + 2 === 4 and TypeScript hands back a boolean before you can blink. The claim itself disappears and only the verdict survives. Every logical expression lands in that same single type.

Lean gives you a Prop

In Lean, 2 + 2 = 4 has type Prop, short for logical proposition. So does 2 + 2 = 5. Being wrong does not change what type it is.

Claims stay claims

A Lean proposition never collapses into true or false. It stays a sentence you can name, hold onto, and hand to other code.

“A proposition remains a proposition”

So compute it? No

You cannot calculate your way to truth here. Adding up 1 + 1/2 + 1/4 + 1/8 and onward to show it equals 2 would need infinite time and memory. Lean makes you argue instead.

“You compute it! Just kidding.”

A proposition is also a type

Here is the twist. 2 = 2 is a value of type Prop, and it is itself a type. A proof is simply any value of that type.

by rfl builds the proof

def proof1 : 2 = 2 := by rfl typechecks. The tactic returns something whose type is literally 2 = 2, which in turn sits under Prop. A two storey tower TypeScript cannot build.

Proving equals typechecking

If the value fits the type, the claim is established. Nothing executes. A tiny kernel just checks that the pieces line up.

“Verifying any mathematical result in Lean is nothing more than typechecking.”

The lonely type

No one can produce a value of type 2 + 2 = 5, barring a sorry or a bad axiom. That type sits there with no inhabitants at all.

Note the Not

Empty is not the same as false. Maybe you were just unlucky. So you prove the negation: Not (2 + 2 = 5) is its own proposition, and by decide supplies a value for it.

False means uninhabited

Once the negation typechecks, nothing can ever inhabit 2 + 2 = 5. It behaves like TypeScript's never, a type whose value you cannot produce without cheating.

“If the proof typechecks, the argument must be correct.”

All proofs are equal

2 + 2 = 4 can be proved by rfl, by decide, or with Mathlib's two_add_two_eq_four. Once checked, Lean treats all three as the same thing.

“In Lean, all proofs of the same proposition are considered equal”

What booleans throw away

A boolean answers the question and forgets it was asked. A TypeScript function guarding a range from 0 to 1 can only throw at runtime, on every single call, forever.

“it erases the knowledge of which facts have been established”

Pass facts as arguments

In Lean the function takes x, a proof that x is at least 0, and a proof that x is at most 1. Call it with 1.2 and the typechecker stops you before anything runs.

“Now anyone who calls this function will also have to supply these two proofs.”

Beyond number literals

Feed it (sin a) squared and norm_num gives up, because a is unknown. You still know things though. A square is non negative, and sine never leaves the band from -1 to 1.

Ask Lean to find it

Write apply? and Lean searches the library. It surfaces sq_nonneg, a proof of anything shaped like foo squared is at least 0, ready to apply to sin a.

The second hole closes

Ask again and out comes sin_sq_le_one, which proves sine squared is at most 1. Both stubs filled, the whole definition typechecks with no sorry left in it.

“Mathlib is just a bunch of open source proofs.”

Truths about uncomputable things

Real.sin cannot be calculated to infinite precision, so the function is marked noncomputable. You can still prove hard facts about it, and about pi, infinite series, and infinite sets.

Behind the by

a = b turns out to be sugar for Eq a b, and Eq is defined in Lean itself as a type that doubles as a function call. Types are values here, so generics are just arguments.

“Yes, it's a function call that returns a type.”

One constructor, no escape

Eq has a single constructor, refl, and it can only ever build Eq a a. That is why Eq 2 3 has no inhabitants, and why 2 = 3 can never be proved. Go play the Natural Number Game.

“it's genuinely thrilling to pass facts around the program and to know they're true.”