Which square roots are irrational?

√2 is the famous one. It isn't special. Every square root of a whole number is irrational unless that number is a perfect square — and a single proof settles all of them at once.

Pick a number above. Below, its square root is shown two ways — as a continued fraction that, for everything but a perfect square, never ends, and as a hunt for a fraction whose square hits n exactly, which (again, unless n is a perfect square) never lands. The reason both fail is one short proof, and Lean's kernel has checked it for every n.

The one proof: descent by remainder

Suppose some fraction squares to n — that is, there are whole numbers a and b (with b > 0) such that a² = n·b². Let r = a mod b be the remainder of a divided by b, so 0 ≤ r < b.

If r = 0, then b divides a: write a = b·m. Substituting, b²·m² = n·b², so n = m² — n was a perfect square. Done.

If r > 0, we descend. Modulo b, a·r ≡ r·r ≡ a·a = n·b² ≡ 0, so b divides a·r: write a·r = b·A. Squaring and using a² = n·b², (b·A)² = (a·r)² = a²·r² = (n·b²)·r² = b²·(n·r²); cancel b² to get A² = n·r² — the same equation, with the smaller denominator r < b.

From any solution we have built a strictly smaller one. But the whole numbers cannot descend forever, so the descent must have stopped at the first branch, r = 0, which reported n = m². So if any fraction squares to n, then n is a perfect square — and if n is not a perfect square, √n is irrational. ∎

No parity. No prime factorisation. No special handling of 2 versus 3 versus 6. The single ingredient is the remainder.

Checked by the kernel, for every n

A program can only ever test finitely many fractions. The argument above is about all of them, so it belongs to a proof assistant. The following is the heart of SqrtN.lean — zero imports, so the only trusted component is Lean's type checker:

/-- If (a/b)² = n then n is a perfect square. Descent on b. -/
theorem sqrt_rational_is_square (n : Nat) :
    ∀ b a : Nat, 0 < b → a * a = n * (b * b) → ∃ k, k * k = n := by
  intro b
  induction b using Nat.strongRecOn with
  | ind b IH =>
    intro a hb h
    rcases Nat.eq_zero_or_pos (a % b) with hr0 | hrpos
    · -- a % b = 0 : b ∣ a, so a = b·m and n = m²
      obtain ⟨m, hm⟩ := Nat.dvd_of_mod_eq_zero hr0
      ⋯
    · -- a % b > 0 : b ∣ a·r, so a·r = b·A and A² = n·r² with r < b
      obtain ⟨A, hA⟩ := dvd_mul_mod n a b h hb
      ⋯
      exact IH (a % b) hrb A hrpos hAA

-- √2, √3, √5, √6, √7 irrational: one line each, all from the theorem above.
#print axioms SqrtN.sqrt_rational_is_square
-- ⊢ 'SqrtN.sqrt_rational_is_square' depends on axioms: [propext]

Every theorem's axiom footprint is [propext] or [propext, Quot.sound] — no sorryAx, no Classical.choice. Reproduce from a fresh checkout in ~1–2 min: bash research/which-roots-are-irrational/lean/install-lean.sh && bash research/which-roots-are-irrational/lean/verify.sh.