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.


Participants

PERSON
AFFILIATION
PERIOD OF STAY
Mohammad Abdulaziz King's College London 09.06.2024 - 28.06.2024
Ilka Agricola Philipps-Universität Marburg 29.07.2024 - 01.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 - 16.08.2024
Mantas Baksys Cambridge University 28.07.2024 - 04.08.2024
Jason Balaci McMaster University 28.07.2024 - 03.08.2024
Andrej Bauer University of Ljubljana 12.05.2024 - 22.05.2024
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
Christopher Birkbeck University of East Anglia 16.06.2024 - 28.06.2024
Frédéric Blanqui INRIA 22.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 30.06.2024 - 12.07.2024
James Davenport University of Bath

06.05.2024 - 05.07.2024

04.08.2024 - 16.08.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
Adrian De Lon Universität Bonn 06.05.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 16.06.2024 - 29.06.2024
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 11.08.2024 - 16.08.2024
Mateja Jamnik University of Cambridge 05.07.2024 - 12.07.2024
Moa Johansson Chalmers University of Technology 07.07.2024 - 13.07.2024
Sara Kalvala University of Warwick 04.08.2024 - 12.08.2024
Michail Karatarakis Radboud University Nijmegen 06.05.2024 - 02.08.2024
Peter Koepke Universität Bonn
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
Angeliki Koutsoukou-Argyraki Royal Holloway, University of London

16.06.2024 - 22.06.2024

25.07.2024 - 05.08.2024

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 09.06.2024 - 21.06.2024
Hyojae Lim Yonsei University 04.08.2024 - 16.08.2024
Alexei Lisitsa University of Liverpool 05.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

29.06.2024 - 13.07.2024

Patrick Massot Carnegie Mellon University 09.06.2024 - 22.06.2024
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 - 12.07.2024
Fredrik Nordvall Forsberg University of Strathclyde 26.05.2024 - 08.06.2024
Rodrigo Ochigame Leiden University 04.08.2024 - 16.08.2024
José Vitor Paiva Miranda de Siqueira University of Cambridge 04.08.2024 - 10.08.2024
Shashank Pathak The University of Manchester 14.07.2024 - 27.07.2024
Lawrence Paulson University of Cambridge 16.06.2024 - 22.06.2024
Christian Pfrang BayStMD 23.06.2024 - 06.07.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
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

13.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 05.07.2024 - 24.07.2024
Natarajan Shankar SRI International Computer Science Laboratory 16.06.2024 - 14.07.2024
Jure Taslak University of Ljubljana 09.06.2024 - 12.07.2024
Nicolas Thiéry Université Paris Saclay 19.05.2024 - 25.05.2024
Davide Trotta National Research Council, ISTI-CNR 25.05.2024 - 20.06.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 06.05.2024 - 16.08.2024
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

12.05.2024 - 18.05.2024

16.06.2024 - 22.06.2024

07.07.2024 - 02.08.2024

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 - 17.05.2024
Baran Zadeoglu Cornell University, Malott Hall 17.06.2024 - 16.08.2024
PERSON
AFFILIATION
Sanskar Agrawal
Guillaume Allais
Thomas Ammer
Santiago Arambillete
Metin Ersin Arican
Kevin Arlin
Matteo Calosci
Madhurima Deb
Manuel Eberl
Mirko Engler
Matthew Foreman
Giorgio Genovesi
Leo Gitin
Tarakaram Gollamudi
Astra Kolomatskaia
Chen-wei (Milton) Lin
Jacob Loader
Krystal Maughan
Sam Owre
Nima Rasekh
Michael Rothgang
Michel Smykalla
Giovanni Solda
James Spence
Dieter Vandesande
David Wang
Freek Wiedijk
IISER Tirupati
University of Strathclyde
King's College London
Université Paris Cité
Bogazici University
Topos Institute
Università degli Studi di Firenze
FIZ Karlsruhe GmbH
Universität Innsbruck
Universität Wien
University of California, Irvine
University of Leeds
University of Oxford
Carnegie Mellon University
Stony Brook University
Johns Hopkins University
University of Cambridge
University of Vermont
SRI International
MPIM Bonn
Humboldt-Universität zu Berlin
University of Sao Paulo
Ghent University
King's College London
Vrije Universiteit Brussel
King's College London
Radboud University 
PERSON
AFFILIATION
PERIOD OF STAY
Mohammad Abdulaziz
Thomas Ammer
Dagur Asgeirsson
Jeremy Avigad
Steve Awodey
Jonas Bayer
Christoph Benzmüller
Katja Bercic
Yves Bertot
Christopher Birkbeck
Kevin Buzzard
Jacques Carette
Mario Carneiro
Alain Chavarri Villarello
Cyril Cohen
Johan Commelin
James Davenport
María Inés de Frutos Fernández
Adrian De Lon
Valeria de Paiva
Mirna Dzamonja
William Farmer
Georges Gonthier
Sina Hazratpour
Michail Karatarakis
Peter Koepke
Andrea Kohlhase
Michael Kohlhase
Angeliki Koutsoukou-Argyraki
Robert Lewis
Maria Emilia Maietti
Patrick Massot
Wojciech Nawrocki
Christine Paulin-Mohring
Lawrence Paulson
Florian Rabe
Emily Riehl
Claudio Sacerdoti Coen
Maximilian Schäffeler
Natarajan Shankar
Jure Taslak
Davide Trotta
Josef Urban
Floris van Doorn
David Wang
Freek Wiedijk
Baran Zadeoglu
King's College London
King's College London
University of Copenhagen
Carnegie Mellon University
Carnegie Mellon University
Cambridge University
University of Bamberg
University of Ljubljana
Inria
University of East Anglia
Imperial College London
McMaster University
Carnegie Mellon University
Vrije Universiteit Amsterdam
Inria
Albert–Ludwigs-Universität Freiburg
University of Bath
Universidad Autónoma de Madrid
Universität Bonn
Topos Institute
IRIF (CNRS et Université Paris Cité)
McMaster University
Inria Saclay Ile de France
Johns Hopkins
Radboud University Nijmegen
Universität Bonn
Neu-Ulm University of Applied Sciences
FAU Erlangen-Nürnberg
Royal Holloway, University of London
Brown University
University of Padova
Carnegie Mellon University
Carnegie Mellon University
Faculté des Sciences, Université Paris-Saclay
University of Cambridge
University Erlangen-Nuremberg
Johns Hopkins University
Alma Mater Studiorum - Università di Bologna
TU Munich
SRI International Computer Science Laboratory
University of Ljubljana
National Research Council, ISTI-CNR
CIIRC - CTU
Universität Bonn
King's College London
Radboud University
Cornell University, Malott Hall
PERSON
AFFILIATION
PERIOD OF STAY
Jeremy Avigad
Katja Bercic
Jacques Carette
Mario Carneiro
Alain Chavarri Villarello
Johan Commelin
Sander Dahmen
Adrian De Lon
Valeria de Paiva
Silvia De Toffoli
Stefania Dumbrava
Sina Hazratpour
Lucy Horowitz
Mateja Jamnik
Romana Jezek
Moa Johansson
Michail Karatarakis
Peter Koepke
Andrea Kohlhase
Michael Kohlhase
Wenda Li
Ursula Martin
Paul-André Melliès
Dennis Müller
Wojciech Nawrocki
Andrei Paskevich
Florian Rabe
Aarne Ranta
Emily Riehl
Jan Frederik Schaefer
Gisele Secco
Natarajan Shankar
Jure Taslak
Nicolas M. Thiéry
Kensho Tsurusaki
Josef Urban
Floris van Doorn
Freek Wiedijk
Baran Zadeoglu
Carlos Zapata-Carratala
Carnegie Mellon University
University of Ljubljana
McMaster University
Carnegie Mellon University
Vrije Universiteit Amsterdam
Albert–Ludwigs-Universität Freiburg
VU Amsterdam
Universität Bonn
Topos Institute
IUSS Pavia
ENSIIE
Johns Hopkins
University of Chicago
University of Cambridge
University of Vienna
Chalmers University of Technology
Radboud University Nijmegen
Universität Bonn
Neu-Ulm University of Applied Sciences
FAU Erlangen-Nürnberg
University of Edinburgh
Wadham College Oxford
CNRS, Universite Paris Cite, INRIA
FAU Erlangen-Nürnberg
Carnegie Mellon University
Université Paris-Saclay
University Erlangen-Nuremberg
University of Gothenburg
Johns Hopkins University
Friedrich-Alexander-Universität Erlangen-Nürnberg
California State University San Bernardino
SRI International Computer Science Laboratory
University of Ljubljana
Université Paris-Saclay
The University of Tokyo
CIIRC - CTU
Universität Bonn
Radboud University
Cornell University, Malott Hall
Wolfram Institute
 
PERSON
AFFILIATION
PERIOD OF STAY
Ilka Agricola
Jeremy Avigad
Mauricio Ayala Rincon
Mantas Baksys
Jason Balaci
Katja Bercic
Luis Berlioz
Frédéric Blanqui
Jacques Carette
Mario Carneiro
Johan Commelin
Adrian De Lon
Valeria de Paiva
Yannick Forster
Sina Hazratpour
Fabian Huch
Michail Karatarakis
Peter Koepke
Andrea Kohlhase
Michael Kohlhase
Angeliki Koutsoukou-Argyraki
Heather Macbeth
Assia Mahboubi
Paul-André Melliès
Pietro Monticone
Dennis Müller
Florian Rabe
Aarne Ranta
Emily Riehl
Claudio Sacerdoti Coen
Moritz Schubotz
Marcel Schütz
Kensho Tsurusaki
Josef Urban
Floris van Doorn
Makarius Wenzel
Freek Wiedijk
Baran Zadeoglu
Philipps-Universität Marburg
Carnegie Mellon University
Universidade de Brasília
Cambridge University
McMaster University
University of Ljubljana
Universidad Nacional Autónoma de Honduras
INRIA
McMaster University
Carnegie Mellon University
Albert–Ludwigs-Universität Freiburg
Universität Bonn
Topos Institute
Centre Inria de Paris
Johns Hopkins
Technische Universität München
Radboud University Nijmegen
Universität Bonn
Neu-Ulm University of Applied Sciences
FAU Erlangen-Nürnberg
Royal Holloway, University of London
Fordham University
Inria
CNRS, Universite Paris Cite, INRIA
University of Trento
FAU Erlangen-Nürnberg
University Erlangen-Nuremberg
University of Gothenburg
Johns Hopkins University
Alma Mater Studiorum - Università di Bologna
FIZ Karlsruhe
FAU Erlangen-Nürnberg
The University of Tokyo
CIIRC - CTU
Universität Bonn
Dr. Wenzel, Augsburg
Radboud University
Cornell University, Malott Hall
 

Trimester Seminar Series

Video Recordings

For details concerning the seminar series, please see here (will be updated every friday)


  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)

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.


Informal workshop on formalising the global Langlands conjectures

June 10 - 14, 2024 

Venue: HIM lecture hall, Poppelsdorfer Allee 45, Bonn

Kevin Buzzard will be giving some lectures at HIM on the current state of the project to formalise Fermat's Last Theorem in Lean. The lectures will be suitable for master's students and above interested in formalisation and number theory. During the week he will suggest many formalisation topics to work on and guide the attendees through how to contribute to the project via individual or group work. Most of the time will be spent working on Lean projects. Anyone interested is welcome, including Lean beginners, although you would be better off if you've worked through some of the free online textbook "Mathematics in Lean"

We will be focussing on defining automorphic forms, stating profound theorems linking them to Galois representations, and also stating R=T theorems. We will need to formalise Masters level mathematics across number theory, geometry, analysis and algebra, and will focus on whatever the strengths of the audience are.

We will start every day formally with a lecture 11-12 in the HIM lecture hall.

Wird geladen