Wenda Li is a lecturer in hybrid AI at the University of Edinburgh and a visiting research fellow at the University of Cambridge. Prior to this, he was a research associate and a PhD student working with Prof. Larry Paulson at the University of Cambridge.
His research interest includes
neuro-symbolic reasoning,
AI for math,
machine learning for theorem proving,
and mechanised mathematics.
He is hoping to explore better neuro-symbolic frameworks for mathematical reasoning. His research has been funded by Renaissance Philanthropy and ARIA.
Feel free to get in touch if you’re interested in collaborating or pursuing a PhD under my supervision — fully funded positions for international students are available. Due to the high volume of queries I receive, please excuse me if I’m unable to respond to everyone.
I’m also looking to fill a postdoc position in LLM-based mathematical reasoning, starting as soon as possible and lasting for two years. Please feel free to get in touch if you’re interested or would like more details.
@inproceedings{yang2024formalmathematicalreasoningnew,title={Formal Mathematical Reasoning: A New Frontier in AI},author={Yang, Kaiyu and Poesia, Gabriel and He, Jingxuan and Li, Wenda and Lauter, Kristin and Chaudhuri, Swarat and Song, Dawn},year={2025},booktitle={International Conference on Machine Learning},}
ITP
Formalising Half of a Graduate Textbook on Number Theory
Manuel Eberl, Anthony Bordg, Lawrence Paulson, and 1 more author
In International Conference on Interactive Theorem Proving, 2024
@inproceedings{zhou2024dont,title={Formalising Half of a Graduate Textbook on Number Theory},author={Eberl, Manuel and Bordg, Anthony and Paulson, Lawrence and Li, Wenda},booktitle={International Conference on Interactive Theorem Proving},year={2024},}
@misc{jiang2023multilingual,title={Multi-language Diversity Benefits Autoformalization},author={Jiang, Albert Q. and Li, Wenda and Jamnik, Mateja},year={2024},booktitle={Conference on Neural Information Processing Systems,}}
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
@inproceedings{jiang2023draft,title={Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},author={Jiang, Albert Qiaochu and Welleck, Sean and Zhou, Jin Peng and Lacroix, Timothee and Liu, Jiacheng and Li, Wenda and Jamnik, Mateja and Lample, Guillaume and Wu, Yuhuai},booktitle={The Eleventh International Conference on Learning Representations },year={2023},}
NeurIPS
Autoformalization with large language models
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, and 4 more authors
Advances in Neural Information Processing Systems, 2022
@article{wu2022autoformalization,title={Autoformalization with large language models},author={Wu, Yuhuai and Jiang, Albert Qiaochu and Li, Wenda and Rabe, Markus and Staats, Charles and Jamnik, Mateja and Szegedy, Christian},journal={Advances in Neural Information Processing Systems},year={2022},}
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
@inproceedings{li2021isarstep,title={IsarStep: a Benchmark for High-level Mathematical Reasoning},author={Li, Wenda and Yu, Lei and Wu, Yuhuai and Paulson, Lawrence C.},booktitle={International Conference on Learning Representations,},year={2021},}
JAR
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
@article{li2020evaluating,title={Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL},author={Li, Wenda and Paulson, Lawrence C},journal={Journal of Automated Reasoning},volume={64},number={2},pages={331--360},year={2020},publisher={Springer}}
JAR
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
Wenda Li, Grant Olney Passmore, and Lawrence C Paulson
@article{li2019deciding,title={Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL},author={Li, Wenda and Passmore, Grant Olney and Paulson, Lawrence C},journal={Journal of Automated Reasoning,},volume={62},number={1},pages={69--91},year={2019},publisher={Springer}}
