AIAI Seminar: Monday 21st September 2026 by Wenda Li

Title: AI for (Formal) Theorem Proving

Abstract: Large language models have demonstrated remarkable capabilities in mathematical theorem proving and autoformalisation. Recent milestones include Anthropic's autoformalisation of Fermat's Last Theorem in Lean and OpenAI's claimed resolution of the Navier–Stokes problem, which was released together with a Lean formalisation. In this talk, I will give an overview of AI for (formal) theorem proving: a brief history of the field, the key methodologies, and the benchmarks used to measure progress. The talk is adapted from my ICML 2026 tutorial, Proving Theorems with Lean and Machine Learning (https://leanmachinelearning.org/icml-tutorial/), updated to reflect these latest developments.

Bio: Wenda Li is a Lecturer in Hybrid AI in the School of Informatics at the University of Edinburgh, working on proof assistants and machine learning for theorem proving. He and his student co-pioneered autoformalisation with large language models, and he has contributed to several neural theorem-proving systems, including DeepSeek-Prover, Seed-Prover and the Numina Lean Agent. His research is supported by the AI for Math Fund from Renaissance