Paper
Ueber eine elementare Frage der Mannigfaltigkeitslehre, 1891. Jahresbericht der Deutschen Mathematiker-Vereinigung, vol. 1, pp. 75–78. Read the original text and an English translation.
Connection to the paper
The opening diagonal argument considers infinite sequences made from two symbols. This reconstruction represents those symbols as Lean’s Bool values and the sequences as functions from Nat to Bool. The statement here is a modern paraphrase, not a quotation.
The result
No list indexed by the natural numbers can contain every infinite sequence of two symbols.
d(n) = ¬ list(n)(n)
Proof in plain English
- Imagine a list. Each row is an infinite sequence of two symbols. Even if the list has infinitely many rows, it may still miss a sequence.
- Change the diagonal. Build a new sequence: flip the first symbol in the first row, the second symbol in the second row, and so on.
- Find the mismatch. At position n, the new sequence disagrees with row n. So it cannot equal that row. This works for every n, which means it is missing from the whole list.
Scope & assumptions
The diagonal construction and the conclusion that no natural-number-indexed list contains all Boolean sequences. The rest of Cantor’s paper, general cardinal comparisons, and the connection to real numbers are outside this artifact.
The proposed list is arbitrary, and its sequences are infinite functions rather than finite arrays. No assumption about how the list is computed is needed. The proof does not use classical excluded middle or choice.
Notation in Lean
| Meaning | Lean |
|---|---|
| An infinite sequence of two symbols | Sequence := Nat → Bool |
| A proposed enumeration | list : Nat → Sequence |
| The sequence built along the diagonal | diagonal list |
| Different from every row | diagonal_not_in_list |
| No enumeration contains every sequence | no_complete_list |
Lean proof
/-
Paper to Lean · Cantor's diagonal argument
Georg Cantor, Ueber eine elementare Frage der Mannigfaltigkeitslehre (1891).
Scope: the diagonal construction for infinite sequences of two symbols.
This is a modern reconstruction of the selected argument, not the entire paper.
Lean 4.33.1; only Lean's automatically imported core library is needed.
Run: lean -DwarningAsError=true Cantor.lean
License: MIT (see the project LICENSE).
-/
namespace PaperToLean.Cantor
-- A sequence is an infinite stream of two possible symbols.
abbrev Sequence := Nat → Bool
-- Given a proposed list, flip its nth sequence's nth symbol.
def diagonal (list : Nat → Sequence) : Sequence :=
fun n => !(list n n)
-- The new sequence differs from each listed sequence at its own index.
theorem diagonal_not_in_list (list : Nat → Sequence) (n : Nat) :
diagonal list ≠ list n := by
intro h
have same := congrArg (fun sequence => sequence n) h
change (!(list n n)) = list n n at same
cases value : list n n <;> simp [value] at same
-- Consequently, no natural-number-indexed list contains every sequence.
theorem no_complete_list :
¬ ∃ list : Nat → Sequence, ∀ sequence, ∃ n, list n = sequence := by
intro ⟨list, complete⟩
obtain ⟨n, equal⟩ := complete (diagonal list)
exact diagonal_not_in_list list n equal.symm
#print axioms diagonal_not_in_list
#print axioms no_complete_list
end PaperToLean.Cantor
Inspect the verification record
Lean reports propext (propositional extensionality), used by the simplifier in this proof. There are no custom axioms or unfinished proof placeholders.
Lean 4.33.1
Dependencies: Lean core
File: Cantor.lean
SHA-256: 48ea27acf2bb8fb6c5402fbfa50fa9f5247c7feb4b35c13c30c217b44c5f506e
Result: passed
'PaperToLean.Cantor.diagonal_not_in_list' depends on axioms: [propext]
'PaperToLean.Cantor.no_complete_list' depends on axioms: [propext]
SHA-256: 48ea27acf2bb8fb6c5402fbfa50fa9f5247c7feb4b35c13c30c217b44c5f506e
Run it
Install Lean with elan, download Cantor.lean, then run:
lean +leanprover/lean4:v4.33.1 -DwarningAsError=true Cantor.lean