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.

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.

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