Irrationality of √2
A closed, sorry-free proof that √2 is irrational, done by infinite descent rather than by invoking Mathlib's existing theorem. Euclid's infinitude of primes sits alongside as a second complete argument. This is the primer: a finished tree you can read end to end.
√2 is irrational
Status: proved
Irrational (Real.sqrt 2)
No rational squares to 2
Status: proved
∀ x : ℚ, x² ≠ 2
No natural solution of p² = 2q²
Status: proved
∀ p q : ℕ, q ≠ 0 → p² ≠ 2q²
Infinitely many primes
Status: proved
∀ n, ∃ p ≥ n, p.Prime