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.
News
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
- Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson IsarStep: a Benchmark for High-level Mathematical Reasoning Accepted for the Ninth International Conference on Learning Representations, ICLR 2021.
- Wenda Li and Lawrence Paulson Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL Journal of Automated Reasoning, 2019. [pdf]
- Wenda Li and Lawrence Paulson Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem Proceedings of the 8th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2019. [pdf]
- Wenda Li, Grant Passmore and Lawrence Paulson Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL Journal of Automated Reasoning, 2017. [pdf][code]
- Wenda Li and Lawrence Paulson A formal proof of Cauchy's residue theorem Proceedings of the 7th International Conference on Interactive Theorem Proving, ITP 2016.[pdf,slide]
- Wenda Li and Lawrence Paulson A modular, efficient formalisation of real algebraic numbers Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016.[pdf,slide]
Thesis
Archive of Formal Proofs
Contact
Computer Laboratory
University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
wl302 (at) cam.ac.uk