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