Wenda Li


AIAI, Informatics Forum,

University of Edinburgh,

10 Crichton Street,

Edinburgh EH8 9AB, UK

I am a lecturer in hybrid AI at the University of Edinburgh and a visiting research fellow at the University of Cambridge. Prior to this, I was a research associate and a PhD student working with Prof. Larry Paulson at the University of Cambridge.

My research interest includes

  • machine learning for theorem proving,
  • interactive theorem proving,
  • verified symbolic computing,
  • and mechanised mathematics.

I believe modern machine learning techniques will revolutionise the way people do mechanised proofs, so that we can build more reliable systems.

Feel free to drop me an email if you are interested in my research and want to have a project with me (PhD, MSc, summer intern, etc.).

selected publications

  1. ICLR (oral)
    Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, and 6 more authors
    In The Eleventh International Conference on Learning Representations 2023
  2. NeurIPS
    Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
    Albert Q Jiang, Wenda Li, Szymon Tworkowski, and 5 more authors
  3. ICML
    Lime: Learning inductive bias for primitives of mathematical reasoning
    Yuhuai Wu, Markus N Rabe, Wenda Li, and 3 more authors
    In International Conference on Machine Learning, 2021
  4. ICLR
    IsarStep: a Benchmark for High-level Mathematical Reasoning
    Wenda Li, Lei Yu, Yuhuai Wu, and 1 more author
    In International Conference on Learning Representations, 2021
  5. JAR
    Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
    Wenda Li, and Lawrence C Paulson
    Journal of Automated Reasoning 2020
  6. JAR
    Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
    Wenda Li, Grant Olney Passmore, and Lawrence C Paulson
    Journal of Automated Reasoning, 2019