Wenda Li

Lecturer in University of Edinburgh

Wenda Li is a Lecturer in Hybrid AI at the University of Edinburgh, specialising in AI for mathematics. He has contributed to pioneering work on autoformalisation using large language models and explored approaches for guiding formal theorem proving with informal proofs. Beyond this, his work also spans verified quantifier elimination, Grothendieck’s scheme theory, and aspects of analytic number theory. His achievements in these areas were recognised as a runner-up for the BCS Best Dissertation Award.

Talk

Title: Will mathematical theorem proving be solved by scaling laws?

Abstract: 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 compute, 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.