# 4th - A Very Mathematical Dilemma: Alan Bundy, University of Edinburgh

The 4th Annual Boole Lecture in Informatics was given by Prof. Alan Bundy, School of Informatics, University of Edinburgh on Monday 20th February 2006 in Boole 1, UCC at 8pm

Title: "A Very Mathematical Dilemma"

Abstract: Mathematics is facing a dilemma at its heart: the nature of mathematical proof. We have known since Turing showed that mathematical provability was undecidable, that there are theorems with short statements, but with only enormous proofs. Within the last half century we have discovered practical examples of such theorems: the classification of all finite simple groups, the Four Colour Theorem and Kepler's Conjecture. These theorems were only proved with the aid of a computer. But computer proof is very controversial, with many mathematicians refusing to accept a proof that has not been thoroughly checked and understood by a human. The choice seems to be between either abandoning the investigation of theorems with only enormous proofs or changing traditional mathematical practice to include computer-aided proofs. Or is there a way to make large computer proofs more accessible to human mathematicians?