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 rhn_mk1 on Thursday January 19, 2023 @06:42AM (#34439275)

Thanks, this is actually a much better description, especially 4. OP's description can be used to "prove" that 1/2 is irrational.

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by thaumasiotes on Thursday January 19, 2023 @07:45AM (#34439713)

> OP's description can be used to "prove" that 1/2 is irrational.

That won't work; in that case, k' will not be a positive number (k/2 - k is negative whenever k is positive), so you'll fail to produce a contradiction.

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by rhn_mk1 on Thursday January 19, 2023 @08:14AM (#34439915)

Fair enough. Take 3/2 in that case.

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by hgsgm on Thursday January 19, 2023 @08:39AM (#34440097)

Doesn't work, because in

    k * (3/2 - 1)(3/2) = k'(9/4) - k(3/2)

(3/2)^2 = 9/4 is not an integer, you don't get k' < K so there is no contradiction.

You'd only get an integer if 4 divides k', which doesn't happen, because

    k = 2

and

    k' = k(3/2 -1) = k/2 = 1

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by rhn_mk1 on Thursday January 19, 2023 @09:03AM (#34440353)

Thanks, you're right. I missed that there was supposed to be a √2*√2 in the expansion of the last line.

[ Parent | on HN ]