Formalising a new proof that the square root of two is irrational | Hacker News Reader