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.
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
|
Philipps-Universität Marburg
|
|
For details concerning the seminar series, please see here (will be updated every friday)
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.
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.
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.
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.
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.