Desciption
The 2024 HIM Trimester Program on “Prospects of Formal Mathematics” brought together researchers from theorem proving, formal verification, computer algebra, mathematical knowledge management, artificial intelligence, and mainstream mathematics. The program highlighted both the progress of formalized mathematics and the growing interaction between formal methods and mathematical practice.
This follow-up workshop aims to revisit some of the central questions discussed during the trimester, assess developments since 2024, and identify promising directions for future research. Since the trimester, advances in proof assistants, mathematical libraries, automated reasoning, and AI-based tools have continued at a rapid pace, creating new opportunities as well as new conceptual and practical challenges.
The workshop will focus in particular on the following broad questions:
- How can formal systems become more integrated into ordinary mathematical practice and communication?
- What role will AI and automated reasoning play in the development, verification, and exploration of mathematics?
- How can formalization contribute not only to correctness, but also to human understanding, explanation, and insight in mathematics?
- How should large formal mathematical libraries be organized, maintained, and interconnected across different systems and communities?
- What new forms of collaboration between mathematicians, computer scientists, logicians, and educators are needed to shape the future of formal mathematics?
The workshop will provide a forum for discussion among researchers from different communities and formal systems, with the goal of strengthening existing collaborations and fostering new interactions across disciplines.
Scientific Organizers:
- Kevin Buzzard (London)
- Jacques Carette (Hamilton)
- Valeria de Paiva (Berkeley)
- Michael Kohlhase (Erlangen)
- Josef Urban (Praha)