Hausdorff School: “Formal Mathematics and Computer-Assisted Proving”
Dates: September 18 - 22, 2023
Venue: Lipschitz-Saal (Endenicher Allee 60, Bonn)
Organizers: Philipp Hieronymi (Bonn), Peter Koepke (Bonn), Petra Mutzel (Bonn), Heiko Röglin (Bonn)
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:
- Floris van Doorn (University of Paris-Saclay): Interactive theorem proving in LEAN
- TBA: Type-theoretic foundations of interactive theorem provers
- TBA: Automated and computer-assisted theorem
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.
Please send applications using the form below, the deadline for applications is April 5, 2023.
In case of scientific questions, please contact the organizers at formalmaths(at)hcm.uni-bonn.de, in case of questions concerning services and administration, please contact hsm(at)hcm.uni-bonn.de.