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 ummonk on Thursday January 19, 2023 @04:57AM (#34438541)

This is similar to the proof of the fundamental theorem of arithmetic (from which the irrationality of the square root of 2 trivially follows): https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithme...

[ Parent | on HN ]

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

This sort of contradiction by infinite descent is not uncommon: e.g. the textbook proofs of Fermat’s last theorem for n = 3 and 4, or the proof that a periodic crystal lattice can only have symmetry axes of order {1,2,3,4,6}.

[ Parent | on HN ]