Weitere Informationen zum ausgewählten Kolloquiumsvortrag:

Pure mathematics in crisis?

Prof. Kevin Buzzard, Imperial College

Donnerstag, 2019-04-25 17:00Uhr

What is a rigorous mathematical proof? In mathematics departments we teach the undergraduates the answer to this question: a proof is a series of logical deductions, each one justified by previous conclusions and the axioms of mathematics. In my talk I will argue that the "proofs" that we produce in our research are not of this nature at all. The main reason for this is that mathematical proofs in the literature are written by humans, and hence contain omissions (often) and errors (occasionally). Some of the errors are unfixable, and some of the omissions are serious. I will speak about practical consequences of this, giving explicit examples of issues across pure mathematics. Many modern proofs rely on ideas which are "known to the experts", and sometimes there is no satisfactory treatment of these ideas in the literature. In some cases these experts are dying out and are not being replaced. If our work is not reproducible, is it actually mathematics?

I used to be an algebraic number theorist until recently, but after I began to worry about these issues I spent a year learning how computer scientists do formally verified mathematics using computer proof systems. Not only did this change the way I thought about research but it also changed the way I taught. I now use these computer tools as part of our basic introduction to proof course at Imperial College London.

I will talk about the problems I believe are facing pure mathematics, and to what extent computers can help to solve them.