Formalising a new proof that the square root of two is irrational

Re:Formalising a new proof that the square root of two is ir... by jacobn on Thursday January 19, 2023 @10:34AM (#34441392)

For clarity: the proof hinges on (√2 - 1) < 1 (so that k’ < k) and √2 being a square root so that you can multiply k’ by it and indeed get 2 k - k √2.

This is why it also works for √3, but doesn’t work for √5 or 1.5

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by perihelions on Thursday January 19, 2023 @11:05AM (#34441783)

Right. It can also generalize for any non-integral square root of an integer √n. Let a be the integer ⌊√n⌋, such that a < √n < a+1 -- strict inequalities, because √n is non-integral. So 0 < √n - a < 1 and the same proof works with

    k' = √n k - a k         (instead of √2 k - 1 k)
       = k(√n - a)          (so 0 < k' < k)

    √n k' = n k - a k √n    (is integral; k' ∈ K)

[ Parent | on HN ]