Universität Bonn

Trimester Program: "Prospects of formal mathematics"

May 6 - August 16, 2024

Organizers: Kevin Buzzard, Jacques Carette, Michael Kohlhase, Valeria de Paiva, Josef Urban

Description: Formal Mathematics, the program to formalize, check, and manage mathematical knowledge, statements and proofs with computer support, is about to reach a critical threshold where it can efficiently support mathematical research and teaching. It has the chance to profoundly change practices in pure mathematics, as computer algebra systems have already changed computational and experimental mathematics.
Computer-checked formalizations of mathematical theories can be seen as the kind of complete presentations that Euclid or Bourbaki were aiming for. Formalized results are absolutely correct (modulo remote chances of computer failures) and can be verified by simple ``mechanical'' methods independent of high-level mathematical intuitions, abilities or traditions. They constitute a solid canon of results on which further work can be founded.

An Isabelle Proof of Cantor's Theorem
Most observers agree that methods and tools of Formal Mathematics will eventually enter ordinary mathematical practice on a broad scale. When and how this will happen is an open question that the trimester aims to help solve. Currently proofs accepted by proof assistants appear much like computer code; the discrepancy between formal and normal proofs has so far been a main obstacle against the wider adoption of Formal Mathematics.

The goal of this program is to bring together experts of Formal Mathematics, exploit their interactions, foster future collaborations, and interface them better with the mathematical mainstream. At the same time the goal is to provide a platform for junior researchers to enter Formal Mathematics. A central, unifying theme is to break down adoption barriers of formal methods in Mathematics.

Further Planned Activities: The trimester will organize work into regular get-togethers: e.g. weekly seminars, informal workshops, and open problem sessions.

The online application is closed. For the application to the school, please see here.


Mohammad Abdulaziz King's College London
Ilka Agricola Philipps-Universität Marburg 28.07.2024 - 02.08.2024
Thomas Ammer King's College London 16.06.2024 - 28.06.2024
Dagur Asgeirsson University of Copenhagen 09.06.2024 - 22.06.2024
Jeremy Avigad Carnegie Mellon University 01.06.2024 – 03.08.2024
Steve Awodey Carnegie Mellon University 12.05.2024 – 22.06.2024
Mauricio Ayala Rincon Universidade de Brasilia 28.07.2024 - 10.08.2024
Mantas Baksys Cambridge University 26.07.2024 - 05.08.2024
Jason Balaci McMaster University 26.07.2024 - 03.08.2024
Andrej Bauer University of Ljubljana
Jonas Bayer Cambridge University 09.06.2024 - 28.06.2024
Katja Bercic University of Ljubljana

12.05.2024 - 18.05.2024

09.06.2024 - 02.08.2024

Luis Berlioz Universidad Nacional Autónoma de Honduras 28.07.2024 - 16.08.2024
Alexander Best King's College London 16.06.2024 - 28.06.2024
Christopher Birkbeck University of East Anglia 16.06.2024 - 28.06.2024
Jasmin Blanchette Ludwig-Maximilians-Universität München
Frédéric Blanqui ENS 22.07.2024 - 02.08.2024
Kristopher Brown Topos Institute 14.07.2024 - 02.08.2024
Kevin Buzzard Imperial College London 09.06.2024 – 22.06.2024
Marco Bright Caminati Lancaster University Leipzig 04.08.2024 - 16.08.2024
Jacques Carette McMaster University 16.06.2024 - 02.08.2024
Mario Carneiro Carnegie Mellon University 06.05.2024 - 02.08.2024
Cipriano Junior Cioffo Università degli Studi di Padova 12.05.2024 - 14.06.2024
Cyril Cohen Inria 16.06.2024 - 29.06.2024
Johan Commelin Albert–Ludwigs-Universität Freiburg

17.06.2024 - 21.06.2024

08.07.2024 - 12.07.2024

29.07.2024 - 02.08.2024

Sander Dahmen VU Amsterdam
James Davenport University of Bath 06.05.2024 - 05.07.2024
María Inés de  Frutos Fernández Universidad Autónoma de Madrid 02.06.2024 - 05.07.2024
Tom de Jong University of Nottingham 26.05.2024 - 08.06.2024
Thaynara Arielly de Lima Universidade Federal de Goiás 04.08.2024 - 16.08.2024
Valeria de Paiva Topos Institute 02.06.2024 – 09.08.2024
Silvia De Toffoli IUSS Pavia 07.07.2024 - 13.07.2024
Maximilian Doré Oxford University 23.06.2024 - 06.07.2024
Stefania Dumbrava ENSIIE 30.06.2024 - 19.07.2024
Mirna Dzamonja IRIF (CNRS et Université Paris Cité) 09.06.2024 - 28.06.2024
Maxwell Fan University of Illinois Urbana-Champaign 04.08.2024 - 16.08.2024
William Farmer McMaster University 16.06.2024 - 22.06.2024
Yannick Forster Centre Inria de Paris 06.05.2024 - 24.05.2024
Natalia Garcia-Colin ScaDS AI 21.05.2024 - 31.05.2024
Georges Gonthier Inria Saclay Ile de France
Massimiliano Gubinelli Universität Bonn
Sina Hazratpour Johns Hopkins 12.05.2024 - 02.08.2024
Lucy Horowitz University of Chicago 30.06.2024 - 13.07.2024
Raheleh Jalali Keshavarz Institute of computer Science, Czech Academy of Sience 04.08.2024 - 16.08.2024
Mateja Jamnik University of Cambridge
Moa Johansson Chalmers University of Technology
Cezary Kaliszyk University of Innsbruck
Michail Karatarakis Radboud University Nijmegen 06.05.2024 - 02.08.2024
Peter Koepke Universität Bonn 06.05.2024 – 16.08.2024
Andrea Kohlhase Neu-Ulm University of Applied Sciences 06.05.2024 - 16.08.2024
Michael Kohlhase FAU Erlangen-Nürnberg 06.05.2024 - 16.08.2024
Konstantin Korovin The University of Manchester 04.08.2024 - 16.08.2024
Angeliki Koutsoukou-Argyraki Royal Holloway, University of London
Christopher Lam University of Illinois, Urbana-Champaign 19.05.2024 - 07.06.2024
Hannah Leung University of Illinois, Urbana-Champaign 04.08.2024 - 16.08.2024
Robert Lewis Brown University
Hyojae Lim Yonsei University 04.08.2024 - 16.08.2024
Alexei Lisitsa University of Liverpool 04.08.2024 - 16.08.2024
Heather Macbeth Fordham University 28.07.2024 - 10.08.2024
Marco Maggesi Università die Firenze 04.08.2024 - 16.08.2024
Assia Mahboubi Inria 14.07.2024 - 02.08.2024
Maria Emilia Maietti University of Padova 03.06.2024 - 21.06.2024
Ursula Martin Wadham College Oxford

09.06.2024 - 22.06.2024

07.07.2024 - 13.07.2024

Patrick Massot Carnegie Mellon University
James McKinna Heriot-Watt-University 04.08.2024 - 16.08.2024
Juan Meleiro Universidade de Sao Paulo 06.05.2024 - 07.06.2024
Paul-André Melliès CNRS, Université Paris Cité, Inria 30.06.2024 - 16.08.2024
Harshit Jitendra Motwani Hong Kong University of Science and Technology 12.05.2024 - 14.06.2024
Reed Mullanix McMaster University 06.05.2024 - 14.06.2024
Dennis Müller FAU Erlangen-Nürnberg 22.07.2024 - 03.08.2024
Yutaka Nagashima 04.08.2024 - 16.08.2024
Apurva Nakade Johns Hopkins University 04.08.2024 - 16.08.2024
An Nan McMaster University 19.05.2024 - 07.06.2024
Wojciech Nawrocki Carnegie Mellon University 16.06.2024 - 29.06.2024
Tobias Nipkow Technische Universität München 28.07.2024 - 02.08.2024
Fredrik Nordvall Forsberg University of Strathclyde 26.05.2024 - 08.06.2024
Rodrigo Ochigame Leiden University 04.08.2024 - 16.08.2024
Shashank Pathak The University of Manchester 14.07.2024 - 27.07.2024
Evan Patterson Topos Institute 14.07.2024 - 27.07.2024
Lawrence Paulson University of Cambridge 17.06.2024 - 21.06.2024
Christian Pfrang BayStMD 23.06.2024 - 06.07.2024
J. D. Phillips Northern Michigan University 04.08.2024 - 16.08.2024
Jelle Piepenbrock Radboud University 04.08.2024 - 16.08.2024
Florian Rabe FAU Erlangen-Nürnberg 16.06.2024 - 16.08.2024
Aarne Ranta University of Gothenburg 07.07.2024 - 02.08.2024
Emily Riehl Johns Hopkins University 12.05.2024 - 02.08.2024
Egbert Rijke University of Ljubljana 04.08.2024 - 16.08.2024
Talia Ringer University of Illinois Urbana-Champaign 06.05.2024 - 24.05.2024
Pietro Sabelli University of Padua 19.05.2024 - 07.06.2024
Claudio Sacerdoti Coen Alma Mater Studiorum - Università di Bologna

27.05.2024 - 13.06.2024

17.06.2024 - 04.07.2024

10.07.2024 - 02.08.2024

Jan Frederik Schaefer FAU Erlangen-Nürnberg 30.06.2024 - 19.07.2024
Maximilian Schäffeler Technische Universität München 09.06.2024 - 28.06.2024
Marcel Schütz FAU Erlangen-Nürnberg 21.07.2024 - 09.08.2024
Gisele Secco California State University San Bernardino 07.07.2024 - 09.08.2024
Natarajan Shankar SRI International Computer Science Laboratory
Jure Taslak University of Ljubljana 09.06.2024 - 12.07.2024
Davide Trotta National Research Council, ISTI-CNR 26.05.2024 - 21.05.2024
Kensho Tsurusaki The University of Tokyo 07.07.2024 - 16.08.2024
Sebastian Ullrich Lean FRO 23.06.2024 - 06.07.2024
Josef Urban CIIRC - CTU 07.05.2024 - 03.08.2024
Rishikesh Vaishnav École normale supérieure Paris-Saclay 14.07.2024 - 27.07.2024
Floris van Doorn Universität Bonn
David Wang King's College London 16.06.2024 - 29.06.2024
Jonathan Weinberger Johns Hopkins University 14.07.2024 -27.07.2024
Makarius Wenzel Dr. Wenzel, Augsburg 22.07.2024 - 02.08.2024
Freek Wiedijk Radboud University
Kobe Wullaert Deft University of Technology 19.05.2024 - 07.06.2024
Carlos Zapata-Carratala Wolfram Institute 01.07.2024 - 14.07.2024
Zsolt Zombori Alfréd Rényi Institute of Mathematics 06.05.2024 - 18.05.2024


Trimester Seminar Series

  Publications & Preprints

School on Formal Mathematics

May 13 - 17, 2024

Venue: HIM lecture hall (Poppelsdorfer Allee 45, Bonn)

Organizers: Michael Kohlhase (Erlangen), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Josef Urban (Praha)


  • TBA

Description: This one-week school teaches practical theorem proving in the three proof assistants with the greatest coverage of (research) Mathematics: Coq, Isabelle and Lean as well as smaller, more specialized systems. Key people from the research groups have indicated their willingness to teach (and supervise practical formalization attempts) in this school, drawing on tutorial material of the various systems. Participants of the school will be asked to work on small formalization projects which eventually could lead to contributions to formalization libraries. There will be a couple of introductory and special lectures.

The application is closed.

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this school, are eligible to attend this event.

Workshop: Formalization of Mathematics

June 17 - 21, 2024

Venue: HIM lecture hall, Poppelsdorfer Allee 45, Bonn

Organizers: Michael Kohlhase (Erlangen), Kevin Buzzard (London), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Josef Urban (Praha)

Description: This workshop is devoted to the central theme of the Trimester: How do current and future developments of Formal Mathematics impact and assist active research in central areas of pure mathematics. Talks will focus on examples of such interactions, as well as on the development of adequate techniques. Some half-days will be reserved for informal demonstrations, collaborations and co-working.

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this workshop, are eligible to attend this event.

Workshop: Bridging between informal and formal

July 8 - 12, 2024

Venue: HIM lecture hall, Poppelsdorfer Allee 45, Bonn

Organizers:  Kevin Buzzard (London), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Michael Kohlhase (Erlangen), Josef Urban (Praha)

Description: This workshop focusses on the man / machine interaction in Formal Mathematics.  Presently, most formal proofs are practically unreadable by average mathematicians, as they appear like specialized computer code. Can this be improved by making proof languages "readable", or by automatic translation from formalizations into a natural language-like format?

On the other hand, can the formalization process be made as natural for mathematicians as typing texts into LaTeX, so that formalization and proof-checking happen concurrently without appreciable extra effort? Can AI-methods help with translations from informal to formal? Could (AI) translation techniques translate parts of the vast corpus of existing mathematical texts into formalizations?

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this workshop, are eligible to attend this event.

Workshop: Libraries of Digital Math

July 29 - August 2, 2024

Venue: HIM lecture hall, Poppelsdorfer Allee 45, Bonn

Organizers: Kevin Buzzard (London), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Michael Kohlhase (Erlangen), Josef Urban (Praha)

Description: This workshop will focus on the organization, modularization, and curation of mathematical libraries. Contributions/talks can address any combinations of the five aspects of the Tetrapod (see Fig. 1). Though the workshop has a primary focus on formal libraries, organizational aspects of informal mathematics (e.g. via ontologies) can be addressed, if they contribute to machine-processing of the mathematical heritage. 

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this workshop, are eligible to attend this event.

Wird geladen