Events and news relevant to the Laboratory for Foundations of Computer Science

[Paul Jackson <Paul.Jackson@ed.ac.uk>]

Hello,

there will be an AIAI Seminar on Monday 21^st September in Informatics Forum G.03 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 Philanthropy.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.