Seminar: Neural Theorem Proving: Past and Future

Neural theorem proving within a proof assistant offers a framework where models learn to prove theorems without hand-crafted algorithms. By scaling up data, model size, and search computer, we can build increasingly capable proving agents. In this talk, I’ll review recent progress in the field 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 the University of Cambridge, where he worked under the supervision of Prof. Larry Paulson. His research focuses on auto formalisation with large language models, neural theorem proving, and the formalisation of mathematics. More details are available on his website: https://wenda302.github.io.