Paul Bernays Lectures 2023
Professor Kevin Buzzard
Kevin Buzzard is Professor of Pure Mathematics at the Imperial College, London. His expertise is in algebraic number theory and he is currently working in the area of formal proof verification.
Buzzard studied mathematics at Trinity College in Cambridge where he also obtained his doctoral degree under the supervision of Richard Taylor. He was a post doctoral researcher at the Institute for Advanced Study in Princeton and at the University of California in Berkeley. In 1998 he was a lecturer, in 2002 a reader and since 2004 his has been a professor at the Imperial College in London. He received the Smith Prize from Cambridge University in 1993, the Whitehead Prize from the London Mathematical Society in 2002, and the Senior Berwick Prize in 2008.
Video recordings
The recordings of all lectures are available on the ETH video portal.
Mathematics and the computer
Lecture 1: Can AI do mathematics?
- Date: Monday, 28 August 2023
- Time: 5.00 p.m.
- Room: HG F 30 (Auditorium Maximum)
Abstract: Large language models like ChatGPT can do all sorts of things – including writing correct computer code. But how good are they at mathematics? Do mathematicians need to start worrying that they will be soon out of a job? More realistically, will we get to the stage where modern computer tools such as large language models and interactive theorem provers will be able to help working mathematicians to do their research? I'll give an overview of where we are and speculate about where we're going.
Lecture 2: What is an interactive theorem prover?
- Date: Tuesday, 29 August 2023
- Time: 5.00 p.m.
- Room: HG E 7
Abstract: I will give a live demo of how to use the Lean interactive theorem prover, and discuss uses, and potential future uses, of such tools in teaching, research, and communication of mathematics.
Lecture 3: The Liquid Tensor Experiment.
- Date: Wednesday, 30 August 2023
- Time: 5.00 p.m.
- Room: HG E 7
Abstract: In December 2020 Peter Scholze raised the question of whether a certain technical result in the Clausen-Scholze theory of condensed mathematics could be formally verified in an interactive theorem prover. Nineteen months later a team led by Johan Commelin and Adam Topaz showed that the answer was "yes". I'll give a background to the theory of condensed mathematics and will then explain what the question was, what it reduced to, and how it was solved by a diverse team of people collaborating effectively online in what is essentially a new way. I will also explain the doors which have been opened because of this work.