AITPM

Logo

Workshop on AI and Theorem Provers in Mathematics

View My GitHub Profile

Workshop on AI and Theorem Provers in Mathematics

This meeting 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.

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

Programme Schedule

The preliminary schedule of the workshop is:

All times are BST (i.e., London, observing daylight saving time).

Detailed Programme

April 8th 2026

Kevin Buzzard: What goes into Formalizing Fermat?

I will talk about my ongoing attempt to teach Lean a proof of Fermat’s Last Theorem. I’ll give a broad talk including an update on where we are, and a discussion on ideas which we’ve tried and issues which have arisen.

Paola Iannone: Teaching with Lean for supporting the transition to university mathematics - current research and future trends

In the past few years Lean, and other interactive theorem provers, have entered the university classrooms. Their use is meant both to prepare the mathematicians of the future and to support the transition to the rigour of university mathematics. Research in mathematics education is investigating the impact on aspects of students’ learning of this new digital technology. In this talk I will map the development of this research presenting its main results so far and some directions for future research.

Lawrence Paulson: AI and Isabelle: experiences and perspectives

Recent weeks have seen dramatic developments in AI and theorem proving. Josef Urban has auto-formalised an entire topology textbook, three times: into Megalodon, HOL Light and Isabelle/HOL. Meanwhile, Hanno Becker and Dominic Mulligan of Amazon Web Services have released a suite of tools aimed at facilitating interoperability between Isabelle and LLMs. We can now work interactively, with an LLM at our elbow, or throw a massive job at an LLM and go away for a week. The author will report some experiences and then ask, where is this taking us?

April 9th 2026

Chelsea Edmonds: A Proof Engineering Perspective on Formalising Combinatorics in Isabelle/HOL

Formalised maths is often viewed primarily as a tool to verify proof correctness, yet focusing solely on this motivation overlooks other significant benefits - such as the potential to uncover new mathematical insights. In this context, we must consider not just if a proof verifies, but how we approach the formalisation process itself. This talk will explore this challenge by viewing the formalisation process from a software engineering perspective. Using the Isabelle/HOL proof assistant, we’ll first explore how core engineering principles such as modularity and extensibility can be applied to model complex mathematical hierarchies and proof patterns. I’ll highlight the benefits this approach offers through some examples in combinatorics, while also introducing some key Isabelle features such as locales which facilitate this. I’ll conclude by offering some perspectives on why these engineering principles are more relevant than ever as generative AI is integrated into proof assistants, in order to fully leverage all the benefits of formalised mathematics.

Yang-Hui He; The AI Mathematician

We argue how AI can assist mathematics in three ways: theorem-proving, conjecture formulation, and language processing. Inspired by initial experiments in geometry and string theory in 2017, we summarize how this emerging field has grown over the past years, and show how various machine-learning algorithms can help with pattern detection across disciplines ranging from algebraic geometry to representation theory, to combinatorics, and to number theory.  At the heart of the programme is the question how does AI help with theoretical discovery, and the implications for the future of mathematics.

Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report

In this talk, we survey preliminary work conducted by my research group at RIMS, Kyoto University, since the fall of 2025 on the long-term project of formalizing IUT (inter-universal Teichmüller theory). This work began with the  organization of this project into various stages (Stages 1～5) and revolves  (not so much around writing complete Lean code for the mathematical content  of IUT in its entirety, but rather) around the idea that Lean can utilized as a  communication tool for recording the precise logical structure of key portions  of the logic of IUT in such a way that Lean code can be used to communicate  this logic in a more precise and effective way than conventional natural language- based mathematical discourse to mathematicians who have professional  expertise in writing Lean code (i.e., who, unlike my research group at RIMS,  have the capacity to generate substantial quantities of professionally written  Lean code). Finally, we discuss in detail, as a sort of case study, the  reorganization into suitable blackboxes, from a Lean formalization-oriented  point of view, of the logic of the final portion “3.11⇒3.12” of the third paper on  IUT, since it is this portion of IUT that has received the most public attention. The skeletal Lean code that we wrote for this portion of IUT constituted a  remarkably successful case of the use of Lean as a communication tool.  

April 10th 2026

Patrick Massot: Teaching mathematics using Verbose Lean

Verbose Lean is a library for the Lean proof assistant whose goal is to help teaching first year undergrad students how to read and write mathematical proofs. It shares a lot of goals and principles with the Coq-Waterproof project. In this talk I will show what it looks like and emphasize the flexibility it brings to teachers. This flexibility allows to tune the amount of help given to students and the level of precision required from them.

Natarajan Shankar Beyond QED: AI, Theorem Proving, and the Quest for Beautiful Proofs

The dramatic evolution of generative AI, fuelled by the convergence of data and compute, opens up new opportunities for synergy between AI and Theorem Proving. The talk addresses the following question: Can we leverage this technology to go beyond QED to scale the abilities of humans at all skill levels to understand, create, and use beautiful mathematics?

Organisers