44. The square root of 2 is irrational

The square root of 2 is irrational: there is no fraction a / b with (a / b)² = 2. Clearing the denominator, that says a * a = 2 * (b * b) has no solution in natural numbers with b > 0. Prove it.

This is a challenge and it is Mathlib-free: there are no real numbers, no ring and no Nat.Prime lemmas, only Lean’s core library. omega handles linear arithmetic but treats a * a as an unknown, so the nonlinear steps are yours.

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.