Seminar: Neural Theorem Proving: Past and Future

Neural theorem proving within a proof assistant off ers a framework where models learn toprove theorems without hand-crafted algorithms. By scaling up data, model size, and searchcompute, we can build increasingly capable proving agents. In this talk, I’ll review recent progress inthe fi eld and highlight some promising directions for future exploration.

Dr Wenda Li is a Lecturer in Hybrid AI at the University of Edinburgh. He earned his PhD from theUniversity of Cambridge, where he worked under the supervision of Prof. Larry Paulson. His researchfocuses on autoformalisation with large language models, neural theorem proving, and theformalisation of mathematics. More details are available on his website: https://wenda302.github.io.