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