Convoluted Proof: √2 is Irrational

A sophisticated proof using Dirichlet's theorem, quadratic reciprocity, and ultrafilters in Lean 4 with Mathlib.

Based on Asaf Karagila's ultrafilter-based proof. This is a formalization of an "awfully sophisticated proof for a simple fact."

Proof Comparison: Quantified

How does this proof compare to the standard one taught in schools?

Metric Standard (Parity) This (Dirichlet+QR) Ultraproduct Version
Lines of Lean code ~3 lines* ~120 lines ~250 lines
Key mathematical fact n² even ⟹ n even Legendre symbol (2|p) = -1 + Łoś's theorem
Deepest dependency Nat.Prime.not_isSquare Nat.infinite_setOf_prime_and_eq_mod + hyperfilter existence
Mathematical era Ancient Greece (~500 BCE) 19th century (Dirichlet 1837) 20th century (Łoś 1955)
Requires "lowest terms"? Yes No No
Choice axiom essential? No No Yes (for ultrafilter)

*Mathlib's irrational_sqrt_two is 1 line, calling into ~100 lines of supporting lemmas

Axioms Used (Lean verification)

All three proofs use the same foundational axioms:

#print axioms irrational_sqrt_2
-- 'irrational_sqrt_2' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms irrational_sqrt_2_ultraproduct
-- 'irrational_sqrt_2_ultraproduct' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms irrational_sqrt_two  -- Mathlib's standard proof
-- 'irrational_sqrt_two' depends on axioms: [propext, Classical.choice, Quot.sound]

The axioms are identical because Mathlib uses Classical.choice pervasively. However, the mathematical dependencies are completely different.

Are They Independent Proofs?

Comparison Verdict Reason
Standard vs. This proof ✓ INDEPENDENT Different core lemmas (parity vs. quadratic residues)
Standard vs. Ultraproduct ✓ INDEPENDENT Different core lemmas
Direct vs. Ultraproduct ⚠ SAME CORE Both use Dirichlet + QR; ultraproduct just packages it

The Key Idea

Instead of the usual proof by contradiction using parity, we use heavy machinery:

  1. Dirichlet's Theorem: There are infinitely many primes p ≡ 3 (mod 8)
  2. Quadratic Reciprocity: For such primes, 2 is NOT a quadratic residue mod p
  3. Ultraproducts: Construct an ultraproduct of fields ℤ/pℤ over these primes
  4. Łoś's Theorem: x² = 2 has no solution in the ultraproduct

If √2 = a/b were rational, then for any sufficiently large prime p (not dividing b), we'd have (a/b)² ≡ 2 (mod p), contradicting that 2 is not a square mod p!

Side-by-Side: Standard vs. This Proof

Standard Proof (Parity)

Assume √2 = a/b in lowest terms
→ a² = 2b²
→ a² is even
→ a is even (a = 2k)
→ 4k² = 2b², so b² = 2k²
→ b is even
→ Both even contradicts "lowest terms"
→ ⊥

Core fact: If n² is even, then n is even

This Proof (Dirichlet + QR)

Assume √2 = a/b
→ a² = 2b²
→ Pick prime p ≡ 3 (mod 8), p > max(a,b)
→ p ∤ b, so b invertible mod p
→ (a/b)² ≡ 2 (mod p)
→ 2 is a square mod p
→ But QR says 2 is NOT a square mod p
→ ⊥

Core fact: Legendre symbol (2|p) = -1 for p ≡ 3 (mod 8)

Core Components

Primes ≡ 3 (mod 8) are Infinite

Using Dirichlet's theorem on primes in arithmetic progressions:

lemma primes_three_mod_eight_infinite :
    primes_three_mod_eight.Infinite := by
  exact Nat.infinite_setOf_prime_and_eq_mod three_unit_mod_eight
Proof relies on:
Nat.infinite_setOf_prime_and_eq_mod — Dirichlet's theorem in Mathlib

2 is Not a Square mod p (for p ≡ 3 mod 8)

By quadratic reciprocity, the Legendre symbol (2|p) = -1 when p ≡ 3 (mod 8):

lemma two_not_square_mod_prime_three_mod_eight (p : ℕ)
    (hp : p.Prime ∧ (p : ZMod 8) = 3) (hp2 : p ≠ 2) :
    ¬IsSquare (2 : ZMod p) := by
  haveI : Fact p.Prime := ⟨hp.1⟩
  have : p % 8 = 3 := ...
  rw [ZMod.exists_sq_eq_two_iff hp2]
  push_neg
  constructor
  · intro h; rw [this] at h; norm_num at h
  · intro h; rw [this] at h; norm_num at h
Key lemma:
ZMod.exists_sq_eq_two_iff — 2 is a square mod p iff p ≡ ±1 (mod 8)

The Contradiction

If √2 = a/b, then a² = 2b². For any prime p > max(a,b) with p ≡ 3 (mod 8):

lemma rational_sqrt_two_contradiction (q : ℚ) (hq : (q : ℝ) = √2) : False := by
  -- Get coprime representation √2 = a/b
  obtain ⟨a, b, hb_pos, _hcop, h_ratio⟩ := rat_to_coprime_pair q hq_pos
  have hsq : a ^ 2 = 2 * b ^ 2 := sqrt_two_eq_ratio_implies_square_eq a b hb_pos h_sqrt_ratio

  -- Find a prime p ≡ 3 (mod 8) with p > max(a,b)
  obtain ⟨p, hp_mem, hbig⟩ : ∃ p ∈ primes_three_mod_eight, max a b < p := by
    simpa using primes_three_mod_eight_infinite.exists_gt (max a b)

  -- p doesn't divide b (since p > b), so 2 is a square mod p
  have sq2_in_Fp : IsSquare (2 : ZMod p) := two_is_square_mod_p p a b hsq hpb

  -- But quadratic reciprocity says 2 is NOT a square mod p
  have not_sq2_in_Fp : ¬ IsSquare (2 : ZMod p) :=
    two_not_square_mod_prime_three_mod_eight p hp_mem hp_ne_2

  -- Contradiction!
  exact not_sq2_in_Fp sq2_in_Fp

Ultraproduct Machinery (Optional Overkill)

The ultraproduct version adds ~130 more lines to package "for almost all p" into a single algebraic object:

The Index Set and Ultrafilter

-- The subtype of primes ≡ 3 (mod 8)
abbrev PrimesMod3_8 : Type := {p : ℕ // p.Prime ∧ (p : ZMod 8) = 3}

-- Non-principal ultrafilter extending the cofinite filter
noncomputable def ultrafilterOnPrimes : Ultrafilter PrimesMod3_8 :=
  hyperfilter PrimesMod3_8  -- ← Requires Axiom of Choice!

-- The ultraproduct ∏_U ZMod p
noncomputable abbrev Ultraproduct : Type :=
  (ultrafilterOnPrimes : Filter PrimesMod3_8).Product FieldFamily

Why Ultraproducts are Overkill Here

The ultraproduct proof shows:

But we only need: "x² = 2 has no solution" holds in one factor (any large p).

It's like proving "this glass contains water" by analyzing the thermodynamic properties of the entire ocean.

Can We Avoid Choice?

Proof Choice Required? Why?
Standard (parity) No* Pure arithmetic + well-ordering
This (direct) No* Just picks one prime
This (ultraproduct) Yes hyperfilter requires Boolean Prime Ideal Theorem

*Mathlib uses Classical.choice pervasively, but the mathematical content doesn't require it

Axioms Used

All proofs use standard mathematical axioms (verified by Lean):

No custom axioms were introduced. The proof is independent of Mathlib's existing irrational_sqrt_two theorem (verified: we don't import or reference it).

Source Code

Full source: github.com/alok/Sqrt2Irrational

Built with Lean 4.26.0-rc2 and Mathlib (latest master).