September 18 - 22, 2023
Lipschitz-Saal (Endenicher Allee 60, Bonn)
Organizers: Philipp Hieronymi (Bonn), Peter Koepke (Bonn), Petra Mutzel (Bonn), Heiko Röglin (Bonn)
Description: The last decade has witnessed tremendous advances in both interactive and automated theorem proving, and we are arguably on the doorstep of a new era, in which interactive theorem provers validate ground-breaking mathematical research in a reasonably short time, as shown in Peter Scholze's Liquid Tensor Experiment.
This new area is driven both by new software and by a growing community of users. In addition, we have seen the advent of new software that guides mathematicians in finding proofs, helps them develop new conjectures or even generates a proof or part of a proof with minimal human input.
This HSM will highlight both these developments.
Lecture series by:
- Jeremy Avigad (CMU): Type-theoretic foundations of interactive theorem provers
- Alexander Bentkamp (Düsseldorf): Automated and computer-assisted theorem proving
- Floris van Doorn (University of Paris-Saclay): Interactive theorem proving in LEAN
- Adam Zsolt Wagner (Worcester Polytechnic Institute): Machine Learning and Theorem Proving
The University of Bonn and HSM are committed to diversity and equal opportunity. We aim to increase the proportion of women in areas where women are underrepresented and to facilitate their careers. We therefore strongly encourage women with relevant qualifications to apply.
The due date for application is expired.
Lecture Slides
Summer_school_Hausdorff_Day_1__RL__1_.pdf
Summer_school_Hausdorff_Day_2__Saliency_analysis__1_.pdf
Summer_school_Hausdorff_Day_3__Transformers_and_Makemore.pdf
