Wenda Li

@misc{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},
  eprint = {2601.14027},
  archiveprefix = {arXiv},
  primaryclass = {cs.AI},
  url = {https://arxiv.org/abs/2601.14027}
}

@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},
  eprint = {2601.18944},
  archiveprefix = {arXiv},
  primaryclass = {cs.AI},
  url = {https://arxiv.org/abs/2601.18944}
}

@misc{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},
  eprint = {2504.19110},
  archiveprefix = {arXiv},
  primaryclass = {cs.CL},
  url = {https://arxiv.org/abs/2504.19110}
}

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

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

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

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

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