News for hackers. Stuff that matters.

A comment on Formalising a new proof that the square root of two is irrational. Parent comment

Re:Formalising a new proof that the square root of two is ir... by mannykannot on Thursday January 19, 2023 @09:58AM (#34440969)
If I am not mistaken, the proof in the article works for √3, and your lemma 1 can be modified by noting that when x > 1, √x > 1 and also 1 < 3 < 4 so 1 < √3 < 2, 0 < √3 - 1 < 1, and k' = k(√3 - 1) < k.
[ Parent | on HN ]

There are no comments on this comment yet.