Wenda Li

I am a lecturer in hybrid AI at the University of Edinburgh and a visiting research fellow at the University of Cambridge. Prior to this, I was a research associate and a PhD student working with Prof. Larry Paulson at the University of Cambridge.

My research interest includes

neuro-symbolic reasoning,
AI for math,
machine learning for theorem proving,
and mechanised mathematics.

I am hoping to explore better neuro-symbolic frameworks for mathematical reasoning.

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.

selected publications

ICML (spotlight)

Formal Mathematical Reasoning: A New Frontier in AI

Kaiyu Yang, Gabriel Poesia, Jingxuan He, and 4 more authors

In International Conference on Machine Learning, 2025

Bib HTML

@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

Bib PDF

@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},
}

NeurIPS

Multi-language Diversity Benefits Autoformalization

Albert Q. Jiang, Wenda Li, and Mateja Jamnik

2024

Bib PDF

@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

Bib PDF

@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},
  url = {https://openreview.net/forum?id=SMa9EAovKMC}
}

NeurIPS

Autoformalization with large language models

Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, and 4 more authors

Advances in Neural Information Processing Systems, 2022

Bib PDF

@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

Bib HTML PDF Code

@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

Wenda Li, and Lawrence C Paulson

Journal of Automated Reasoning, 2020

Bib HTML PDF

@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

Journal of Automated Reasoning,, 2019

Bib HTML PDF Code

@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}
}