Interactive theorem provers: can they help mathematicians?
Event details
| Date | 29.11.2023 |
| Hour | 16:00 › 17:00 |
| Speaker | Professor Kevin Buzzard - Imperial College London |
| Location | |
| Category | Conferences - Seminars |
| Event Language | English |
Assyr Abdulle Lecture - Bernoulli Centre
Abstract : An interactive theorem prover is, amongst other things, a programming language which is sufficiently rich that it can in theory understand modern mathematical research. Two natural questions then arise. First, can these systems understand modern mathematical research _in practice_, and secondly, can they actually help us mathematicians to do it? For many years the answer to both questions was a resounding "no". But recently things have begun to change. There are several examples of recently-proved theorems which have been checked by Lean. Furthermore, interacting with these systems forces you to tidy up your ideas and think clearly about abstractions, which can have unexpected positive practical consequences. Also, modern systems are opening up new possibilities for teaching and communicating mathematics. I will give an overview of what has been going on recently in this area, suitable for mathematicians; no background from computer science will be assumed.
Registration before November 22, 2023 is required - thank you
Abstract : An interactive theorem prover is, amongst other things, a programming language which is sufficiently rich that it can in theory understand modern mathematical research. Two natural questions then arise. First, can these systems understand modern mathematical research _in practice_, and secondly, can they actually help us mathematicians to do it? For many years the answer to both questions was a resounding "no". But recently things have begun to change. There are several examples of recently-proved theorems which have been checked by Lean. Furthermore, interacting with these systems forces you to tidy up your ideas and think clearly about abstractions, which can have unexpected positive practical consequences. Also, modern systems are opening up new possibilities for teaching and communicating mathematics. I will give an overview of what has been going on recently in this area, suitable for mathematicians; no background from computer science will be assumed.
Registration before November 22, 2023 is required - thank you
Links
Practical information
- Informed public
- Registration required
- This event is internal
Organizer
- Bernoulli Centre Institute of Mathematics
Contact
- Prof. Martin Hairer Prof. Maryna Viazovska