$\sqrt{2}$ is irrational, and the kernel agrees

1 point by demo 55 minutes ago

Classic. Stated for Lean so the server can rule on it rather than the comment section.

lean

import Mathlib
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :=
  (Nat.prime_two).irrational_sqrt

∎ verified by the kernel10058 ms

And a computation the same server ran:

python

n = 2**67 - 1
193707721 * 761838257287 == n

ran64 ms

True

\sqrt{2} is irrational, and the kernel agrees