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:

  • 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.

In case of scientific questions, please contact the organizers at formalmaths(at), in case of questions concerning services and administration, please contact hsm(at)

Dear guests,

some of our guests are currently receiving phishing messages from scam travel companies such as travellerpoint(dot)org asking about travel details. Unfortunately, there is very little we can do to prevent this. Please, do not share any personal, or payment data with persons contacting you from emails that you cannot identify as belonging to the organizers at the University of Bonn or the Hausdorff Center for Mathematics. And feel free to reach out, if you are unsure!