Prospects of formal mathematics
Trimester Program
May 6 - August 16, 2024
Organizers: Kevin Buzzard, Jacques Carette, Michael Kohlhase, Valeria de Paiva, Josef Urban
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.