Lawrence Paulson – Proof Assistants: From symbolic logic to real mathematics?
May 18th, 2017 Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally developed in…
