Öffentlicher Vortrag am HIM
Kevin Buzzard: Teaching mathematics to computers
Wann? Freitag, 14. Juni 2024, ab 19:00 Uhr, Ende offen
Wo? Hausdorff Research Institute for Mathematics (HIM), Poppelsdorfer Allee 45, 53115 Bonn
Für wen? für alle Mathematikinteressierten
Bitte beachten:
- Eine vorherige Anmeldung ist erforderlich. Es wird bei Einlass kontrolliert.
- Während der Veranstaltung werden Fotos gemacht und der Vortrag gestreamt und aufgezeichnet. Mit der Teilnahme erklären sich die Teilnehmer*innen bzw. deren Erziehungsberechtigte mit den Foto- und Videoaufnahmen sowie deren Speicherung, Veröffentlichung und Verbreitung einverstanden.
Kevin Buzzard: Teaching mathematics to computers
Teaching mathematics to computers
Kevin Buzzard (Imperial College London)
Abstract:
Computers are nowadays much better than human mathematicians at calculations – they can multiply very large numbers together in a fraction of a second. But researchers in pure mathematics prove theorems. The theorem that there are infinitely many prime numbers cannot be proved by calculating more and more prime numbers – it needs a different approach, via logic and reasoning. It is not difficult to teach a computer the rules of logic and the axioms of mathematics. But then is it possible to go from these axioms, via many centuries of theorems, right up to teaching a computer some modern research mathematics? Recent evidence shows that this is now becoming feasible. Will computers soon be able to help humans prove theorems, or even prove new theorems by themselves? This we do not know. I will give an overview of where things are right now. The talk will be suitable for a general mathematical audience – no expertise in research mathematics or computer theorem provers will be assumed!
Zum Vortragenden
Kevin Buzzard
Kevin Buzzard ist Professor für reine Mathematik am Imperial College in London. Sein Fachgebiet ist die algebraische Zahlentheorie. In den letzten Jahren entwickelte er ein starkes Interesse an der formalen, maschinengestützen Verifikation von mathematischen Beweisen. Zusammen mit Johan Commelin und Patrick Massot gelang es Kevin Buzzard das mathematische Konzept des perfektoiden Raums, welches von Peter Scholze im Rahmen seiner Doktorarbei eingeführt wurde, im Beweisassistenten Lean zu formalisieren. Kevin Buzzard studierte Mathematik am Trinity College in Cambridge, wo er auch bei Richard Taylor promovierte. Nach seiner Promotion war er als Forscher am Institute for Advanced Study in Princeton und an der University of California in Berkeley tätig. Seit 1998 ist er am Imperial College in London, zunächst als Dozent, ab 2002 als Reader und seit 2004 als Professor. Er erhielt 1993 den Smith-Preis der Universität Cambridge, 2002 den Whitehead-Preis der London Mathematical Society und 2008 den Senior Berwick Prize. 2022 war er Plenarsprecher auf dem Internationalen Mathematikerkongress.