Workshop on AI and Theorem Provers in Mathematics
The Workshop on AI and Theorem Provers in Mathematics (AITPM) will explore with leading experts some of the recent developments related to the use of AI and theorem provers in mathematics as well as the perspectives for such future use.
- Attendance is free.
- Venue: Online
- Date: 8. - 10. April 2026
- Registration: Online Form
Given consent by speakers, talks will be recorded and made public after the workshop. We do not plan to record the panel session, which are planned to be highly interactive.
Speakers §
- Kevin Buzzard (Imperial College)
- Yang-Hui He (London Institute for Mathematical Sciences)
- Paola Iannone (University of Edinburgh)
- Shinichi Mochizuki (Research Institute for Mathematical Sciences Kyoto)
- Leonardo De Moura (Amazon Web Services)
- Lawrence Paulson (University Cambridge)
- Chelsea Edmonds (University of Western Australia)
- Patrick Massot (University Paris Saclay)
Programme Schedule §
The preliminary schedule of the workshop is:
- April 8th 2026
- 08:00-09:00 Kevin Buzzard: What goes into Formalizing Fermat?
- 09:15-10:15 Paola Iannone: Teaching with Lean for supporting the transition to university mathematics - current research and future trends
- 10:45-11:45 Lawrence Paulson: AI and Isabelle: experiences and perspectives
- 12:00-13:00 Discussion/panel session
- April 9th 2026
- 08:00-09:00 Chelsea Edmond: A Proof Engineering Perspective on Formalising Combinatorics in Isabelle/HOL
- 09:15-10:15 Yang Hui He
- 10:45-11:45 Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report
- 12:00-13:00 Discussion session
- April 10th 2026
- 15:00-16:00 Patrick Massot: Teaching mathematics using Verbose Lean
- 16:15-17:15 Leonardo De Moura
- 17:45-18:45 Natarajan Shankar
- 19:00-20:00 Discussion/panel session and closure
All times are BST (i.e., London, observing daylight saving time).
Organisers §
- Mohamed Saidi (Department of Mathematics and Statistics, University of Exeter)
- Barrie Cooper (Department of Mathematics and Statistics, University of Exeter)
- Gihan Marasingha (Department of Mathematics and Statistics, University of Exeter)
- Achim D. Brucker (Department of Computer Science, University of Exeter)
- Diego Marmsoler (Department of Computer Science, University of Exeter)