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 programme 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.

Planned Activities: The trimester will organize work into

• Regular get-togethers: e.g. weekly seminars, informal workshops, and open problem sessions
• Formalization Schools (both F2F and online) to get participants into the practice of formalizing mathematical knowledge

Thematic Workshops:

• Formalizations in Modern Mathematics (June 2024)
• Bridging Between Informal and Formal Mathematics (July 2024)
• Libraries of Digitized Mathematics (August 2024)

The online application platform to participate in this trimester program will be accessible approximately one year prior to the start of the program.