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 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 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
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 30.06.2024 - 12.07.2024
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
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 04.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
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
Konstantin Korovin The University of Manchester 04.08.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 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

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
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
Paige North Utrecht University 04.08.2024 - 16.08.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 16.06.2024 - 22.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
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

PERSON
AFFILIATION
PERIOD OF STAY
Sanskar Agrawal
IISER Tirupati
Guillaume Allais
University of Strathclyde
Thomas Ammer
King's College London
Santiago Arambillete
Université Paris Cité
Metin Ersin Arican
Bogazici University
Kevin Arlin
Topos Institute
Matteo Calosci
Università degli Studi di Firenze
Madhurima Deb
FIZ Karlsruhe GmbH
Manuel Eberl
Universität Innsbruck
Mirko Engler
Universität Wien
Matthew Foreman
University of California, Irvine
Giorgio Genovesi
University of Leeds
Leo Gitin
University of Oxford
Tarakaram Gollamudi
Carnegie Mellon University
Astra Kolomatskaia
Stony Brook University
Chen-wei (Milton) Lin
Johns Hopkins University
Jacob Loader
University of Cambridge
Krystal Maughan
University of Vermont
Sam Owre
SRI International
Nima Rasekh
MPIM Bonn
Michael Rothgang
Humboldt-Universität zu Berlin
Michel Smykalla
University of Sao Paulo
Giovanni Solda
Ghent University
James Spence
King's College London
Dieter Vandesande
Vrije Universiteit Brussel
David Wang
King's College London
 Freek Wiedijk
Radboud University 
 
PERSON
AFFILIATION
PERIOD OF STAY
Christoph Benzmüller
Universität Bamberg
Yves Bertot
Inria
Christina Paulin-Moring
Université Paris Saclay
 
 
 
 
PERSON
AFFILIATION
PERIOD OF STAY
 Adrian De Lon
Universität Bonn
 
Romana Jezek
Universität Wien
Wenda Li
University of Edinburgh
Dennis Müller
FAU Erlangen-Nürnberg
Andriy Paskevych
Université Paris Saclay
 
 
PERSON
AFFILIATION
PERIOD OF STAY
 Yannick Forster
Centre Inria de Paris
 
Fabian Huch
TU München
 
Moritz Schubotz
FIZ Karlsruhe
Natarajan Shankar
SRI International Computer Science Laboratoy
 
 
 

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)

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". More details to follow.

Wird geladen