Lean for All

Case 1: Cantor, no list of all subsets🔗

Audit a real Mathlib theorem from start to finish: find it, read it, check its definitions, axioms and proof.

This section is hands-on. You audit a real theorem from Mathlib, the library where Lean's mathematics lives, one checklist step at a time, the way you would audit a file an AI sent you. After each step, a question.

The checklist, from Day 27:

  1. Is it really proved? (sorry, axioms)

  2. Does the statement say what was claimed?

  3. Can the hypotheses all hold?

  4. Are the hypotheses honest?

  5. Do the definitions mean what their names say?

The claim🔗

Cantor's theorem (1891): no set can be matched with all of its subsets. However you assign a subset of S to each element of S, some subset is left over. It is the reason there are different sizes of infinity, and it is famous for a short, clever proof.

Step 1: find the theorem🔗

Mathlib calls it Function.cantor_surjective. Hover over the names to see what they are:

@Function.cantor_surjective : ∀ {α : Type u_1} (f : α → Set α), ¬Function.Surjective f#check @Function.cantor_surjective 
@Function.cantor_surjective : ∀ {α : Type u_1} (f : α → Set α), ¬Function.Surjective f

Some vocabulary: α is any type (any collection of things). Set α is a subset of α. f : α → Set α assigns a subset to each element. Function.Surjective f means every subset is assigned to some element.

Step 2: the definitions🔗

Do not trust the name Surjective. Ask Lean what it means:

def Function.Surjective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop := fun {α} {β} f => ∀ (b : β), ∃ a, f a = b#print Function.Surjective 
def Function.Surjective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop :=
fun {α} {β} f => ∀ (b : β), ∃ a, f a = b

So Function.Surjective f is “for every b there is an a with f a = b”: every target is hit. That is the usual meaning, so the name is honest.

Step 3: hypotheses🔗

The statement has only variables before the conclusion: a type α and a function f. There is no hypothesis, no “if”, so nothing can be impossible and nothing can secretly assume the answer.

Step 4: is it really proved?🔗

'Function.cantor_surjective' does not depend on any axioms#print axioms Function.cantor_surjective 
'Function.cantor_surjective' does not depend on any axioms

No sorry, no made-up axioms, not even the three standard ones. The proof uses pure logic.

Step 5: read the proof🔗

You do not have to read a proof to audit it: Lean checks every step. But Cantor's argument is famous, so here it is in tactics. Hover over the tactics to see the goal before and after each one.

theorem cantor (α : Type) (f : α → Set α) : ¬ Function.Surjective f := α:Typef:α → Set α⊢ ¬Function.Surjective f α:Typef:α → Set αhf:Function.Surjective f⊢ False α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}⊢ False α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:d ∈ f d⊢ Falseα:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:¬d ∈ f d⊢ False α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:d ∈ f d⊢ False α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:d ∈ f dh':¬d ∈ f d⊢ False All goals completed! 🐙 α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:¬d ∈ f d⊢ False α:Typef:α → Set αhf:Function.Surjective fd:αhd:f d = {a | ¬a ∈ f a}h:¬d ∈ f dh':d ∈ f d⊢ False All goals completed! 🐙

The idea: suppose f hits every subset. Look at the diagonal subset of the elements not in their own subset. Some d is sent to it. Is d in its own subset? If yes, the diagonal's rule says it is not. If no, the rule says it is. Both are impossible.

The verdict🔗

Proved with no axioms; the statement says the claim; there are no hypotheses; the definitions are Mathlib's standard ones, which we printed. The audit passes.