Wenda Li

AIAI, Informatics Forum,

University of Edinburgh,

10 Crichton Street,

Edinburgh EH8 9AB, UK

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.

news

Jul 13, 2026	I attended the Thematic Program on AI and Mathematics at the Korea Institute for Advanced Study (KIAS).
Jul 06, 2026	With Rémy Degenne, I presented a tutorial on Proving Theorems with Lean and Machine Learning at ICML 2026 in Seoul.

selected publications

ICML

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Junqi Liu, Zihao Zhou, Zekai Zhu, and 10 more authors

In International Conference on Machine Learning, 2026

Bib HTML

@inproceedings{liu2026numinaleanagentopengeneralagentic,
  title = {Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics},
  author = {Liu, Junqi and Zhou, Zihao and Zhu, Zekai and Santos, Marco Dos and He, Weikun and Liu, Jiawei and Wang, Ran and Xie, Yunzhou and Zhao, Junqiao and Wang, Qiufeng and Zhi, Lihong and Li, Jia and Li, Wenda},
  year = {2026},
  archiveprefix = {arXiv},
  primaryclass = {cs.AI},
  booktitle = {International Conference on Machine Learning},
}

ICLR

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

Qiyuan Xu, Xiaokun Luan, Renxi Wang, and 5 more authors

2026

Bib

@misc{xu2026neuraltheoremprovingverification,
  title = {Neural Theorem Proving for Verification Conditions: A Real-World Benchmark},
  author = {Xu, Qiyuan and Luan, Xiaokun and Wang, Renxi and Leang, Joshua Ong Jun and Wang, Peixin and Li, Haonan and Li, Wenda and Watt, Conrad},
  year = {2026},
  archiveprefix = {arXiv},
  primaryclass = {cs.AI},
  url = {https://arxiv.org/abs/2601.18944}
}

ICML

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

Huajian Xin, Zheng Yuan, Xiaoran Jin, and 2 more authors

In International Conference on Machine Learning, 2026

Bib HTML

@inproceedings{xin2026apebenchevaluatingautomatedproof,
  title = {APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries},
  author = {Xin, Huajian and Yuan, Zheng and Jin, Xiaoran and Fleuriot, Jacques and Li, Wenda},
  year = {2026},
  archiveprefix = {arXiv},
  primaryclass = {cs.CL},
  booktitle = {International Conference on Machine Learning},
}

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

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