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 xurukefi on Thursday January 19, 2023 @06:39AM (#34439252)

That's an interesting proof, because I can easily follow it mechanically, but I have absolute no intuition for it.

[ Parent | on HN ]

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

The minimum k is the denominator of the supposed irreducible fraction p/q=sqrt(2). He is stating that then there is a different irreducible fraction r/s=sqrt(2). This is because you would have

p^2=2q^2

with p and q mutually prime, which is impossible.

Instead of irreducible fractions with coprime numbers, he is doing the “dual” using the minimum possible value of the denominator.

[ Parent | on HN ]