Wenda Li


Department of Computer Science and Technology,

University of Cambridge,

William Gates Building,

15 JJ Thomson Avenue,

Cambridge CB3 0FD, UK

I am a research associate at University of Cambridge, working with Prof. Larry Paulson. 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.

I will be joining the University of Edinburgh as a lecturer (equivalent to assistant professor in the US) in September. I will have full scholarships for home and international students - if you want to pursue a PhD with me, please get in touch.

selected publications

  1. arXiv
    Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
    Xueliang Zhao, Wenda Li, and Lingpeng Kong
  2. 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
  3. NeurIPS
    Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
    Albert Q Jiang, Wenda Li, Szymon Tworkowski, and 5 more authors
  4. 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
  5. 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
  6. 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
  7. 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