- Research Associate
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 NLP technuques like language modelling, which I believe will revolutionize the way we derive formal proofs.
Themes
Publications
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
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 To appear at 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 In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016.[ pdf , slide ]
Thesis
Archive of Formal Proofs
- Angeliki Koutsoukou-Argyraki and Wenda Li Irrationality Criteria for Series by Erdős and Straus Archive of Formal Proofs. 2020.
- Angeliki Koutsoukou-Argyraki and Wenda Li The Transcendence of Certain Infinite Series Archive of Formal Proofs. 2019.
- Wenda Li The Budan-Fourier Theorem and Counting Real Roots with Multiplicity Archive of Formal Proofs. 2018.
- Angeliki Koutsoukou-Argyraki and Wenda Li Irrational Rapidly Convergent Series Archive of Formal Proofs. 2018.
- Wenda Li Count the Number of Complex Roots Archive of Formal Proofs. 2017.
- Wenda Li Evaluate Winding Numbers through Cauchy Indices Archive of Formal Proofs. 2017.
- Wenda Li The Sturm-Tarski Theorem Archive of Formal Proofs. 2014.
- Wenda Li The Königsberg Bridge Problem and the Friendship Theorem Archive of Formal Proofs. 2013.
