Seminars relevant to Informatics

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

Hi, 

a reminder about the seminar at 2pm this afternoon by Wenda Li.  

The seminar will be hybrid.  See below for Teams info.

Best,

Paul.

Microsoft Teams meeting

Join: https://teams.microsoft.com/meet/352797632989325?p=ZD9cZkiYnoPS43Dm3M

Meeting ID: 352 797 632 989 325

Passcode: 4Ea3YP2F

From: Paul Jackson <Paul.Jackson AT ed.ac.uk>
Date: Wednesday, 16 September 2026 at 10:52
To: inf-aiai-seminars AT mlist.is.ed.ac.uk <inf-aiai-seminars AT mlist.is.ed.ac.uk>; LFCS Interest <lfcs-interest AT mlist.is.ed.ac.uk>; 'inf-ianc-talks AT mlist.is.ed.ac.uk' <inf-ianc-talks AT mlist.is.ed.ac.uk>; inf-seminars AT mlist.is.ed.ac.uk <inf-seminars AT mlist.is.ed.ac.uk>
Subject: AIAI Seminar Mon 21 Sep, 14:00, IF G.03: Wenda Li on AI for (Formal) Theorem Proving

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.