Prof. Kevin Buzzard, Imperial College:
Pure mathematics in crisis?
Zeit und Ort
Donnerstag, 25.4.19, 17:00-18:00, Hörsaal II, Albertstr. 23b
Zusammenfassung
What is a rigorous mathematical proof? In mathematics\ndepartments we teach the undergraduates the answer to this question: a\nproof is a series of logical deductions, each one justified by\nprevious conclusions and the axioms of mathematics. In my talk I will\nargue that the "proofs" that we produce in our research are not of\nthis nature at all. The main reason for this is that mathematical\nproofs in the literature are written by humans, and hence contain\nomissions (often) and errors (occasionally). Some of the errors are\nunfixable, and some of the omissions are serious. I will speak about\npractical consequences of this, giving explicit examples of issues\nacross pure mathematics. Many modern proofs rely on ideas which are\n"known to the experts", and sometimes there is no satisfactory\ntreatment of these ideas in the literature. In some cases these\nexperts are dying out and are not being replaced. If our work is not\nreproducible, is it actually mathematics?\n\nI used to be an algebraic number theorist until recently, but after I\nbegan to worry about these issues I spent a year learning how computer\nscientists do formally verified mathematics using computer proof\nsystems. Not only did this change the way I thought about research but\nit also changed the way I taught. I now use these computer tools as\npart of our basic introduction to proof course at Imperial College\nLondon.\n\nI will talk about the problems I believe are facing pure mathematics,\nand to what extent computers can help to solve them.\n