Wenda Li

AIAI, Informatics Forum,

University of Edinburgh,

10 Crichton Street,

Edinburgh EH8 9AB, UK

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 theorem proving.

Please feel free to reach out if you’re interested in collaborating or pursuing a PhD under my supervision.

selected publications

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

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