Wenda Li

I am a research associate in the Programming, Logic, and Semantics Group at the Computer Laboratory of the University of Cambridge, under the supervision of Prof. Lawrence C. Paulson.

I am interested in mechanised mathematics and verified decision procedures in proof assistants. I have been building verified procedures in computer algebra in the Isabelle proof assistant to reason about non-linear arithmetic.

I am also excited about the synergy between automated reasoning and modern machine learning, which I believe will revolutionise the way we derive formal proofs.


I am co-organising the MATH-AI workshop at ICLR 2021. Please consider to participate.

In preparation

  • Yuhuai Wu, Markus Rabe, Wenda Li, Jimmy Ba, Roger Grosse, and Christian Szegedy LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
  • Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence C. Paulson Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
  • Anthony Bordg, Lawrence C. Paulson, Wenda Li. Simple Type Theory is not too Simple: Grothendieck's Schemes in the Proof Assistant Isabelle
  • Journal and conference publications


    Archive of Formal Proofs


    Computer Laboratory
    University of Cambridge
    William Gates Building
    15 JJ Thomson Avenue
    Cambridge CB3 0FD, UK
    wl302 (at) cam.ac.uk