publications

2024

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

2. NeurIPS

   Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe

   Alicja Ziarko, Albert Q. Jiang, Bartosz Piotrowski, and 3 more authors

   In Conference on Neural Information Processing Systems, 2024

   Bib PDF

   @inproceedings{ziarko2024repurposing,
     title = {Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe},
     author = {Ziarko, Alicja and Jiang, Albert Q. and Piotrowski, Bartosz and Li, Wenda and Jamnik, Mateja and Miłoś, Piotr},
     year = {2024},
     booktitle = {Conference on Neural Information Processing Systems,}
   }

3. arXiv

   DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

   Huajian Xin, Daya Guo, Zhihong Shao, and 6 more authors

   2024

   Bib

   @misc{xin2024deepseekprover,
     title = {DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data},
     author = {Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan},
     year = {2024},
     eprint = {2405.14333},
     archiveprefix = {arXiv},
     primaryclass = {id='cs.AI' full_name='Artificial Intelligence' is_active=True alt_name=None in_archive='cs' is_general=False description='Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.'}
   }

4. NeurIPS

   Proving Theorems Recursively

   Haiming Wang, Huajian Xin, Zhengying Liu, and 8 more authors

   In Conference on Neural Information Processing Systems, 2024

   Bib PDF

   @inproceedings{wang2024proving,
     title = {Proving Theorems Recursively},
     author = {Wang, Haiming and Xin, Huajian and Liu, Zhengying and Li, Wenda and Huang, Yinya and Lu, Jianqiao and Yang, Zhicheng and Tang, Jing and Yin, Jian and Li, Zhenguo and Liang, Xiaodan},
     year = {2024},
     booktitle = {Conference on Neural Information Processing Systems,}
   }

5. NeurIPS

   End-to-End Ontology Learning with Large Language Models

   Andy Lo, Albert Q. Jiang, Wenda Li, and 1 more author

   2024

   Bib PDF

   @misc{andy2024ontology,
     title = {End-to-End Ontology Learning with Large Language Models},
     author = {Lo, Andy and Jiang, Albert Q. and Li, Wenda and Jamnik, Mateja},
     year = {2024},
     booktitle = {Conference on Neural Information Processing Systems,}
   }

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

7. ICLR

   Don’t Trust: Verify – Grounding LLM Quantitative Reasoning with Autoformalization

   Jin Peng Zhou, Charles E Staats, Wenda Li, and 3 more authors

   In The Twelfth International Conference on Learning Representations 2024

   Bib PDF

   @inproceedings{zhou2024donu,
     title = {Don't Trust: Verify -- Grounding {LLM} Quantitative Reasoning with Autoformalization},
     author = {Zhou, Jin Peng and Staats, Charles E and Li, Wenda and Szegedy, Christian and Weinberger, Kilian Q and Wu, Yuhuai},
     booktitle = {The Twelfth International Conference on Learning Representations},
     year = {2024},
     url = {https://openreview.net/forum?id=V5tdi14ple}
   }

8. PNAS

   Evaluating Language Models for Mathematics through Interactions

   Katherine M. Collins, Albert Q. Jiang, Simon Frieder, and 11 more authors

   2024

   Bib HTML PDF

   @article{collins2023evaluating,
     title = {Evaluating Language Models for Mathematics through Interactions},
     author = {Collins, Katherine M. and Jiang, Albert Q. and Frieder, Simon and Wong, Lionel and Zilka, Miri and Bhatt, Umang and Lukasiewicz, Thomas and Wu, Yuhuai and Tenenbaum, Joshua B. and Hart, William and Gowers, Timothy and Li, Wenda and Weller, Adrian and Jamnik, Mateja},
     year = {2024},
     booktitle = {Proceedings of the National Academy of Sciences 121.24 (2024): e2318124121.},
   }

9. ICML

   Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

   Xueliang Zhao, Wenda Li, and Lingpeng Kong

   In International Conference on Machine Learning 2024

   Bib HTML PDF

   @inproceedings{zhao2023decomposing,
     title = {Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving},
     author = {Zhao, Xueliang and Li, Wenda and Kong, Lingpeng},
     year = {2024},
     booktitle = {International Conference on Machine Learning},
   }

2023

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

2022

1. NeurIPS

   Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

   Albert Q Jiang, Wenda Li, Szymon Tworkowski, and 5 more authors

   2022

   Bib HTML PDF

   @article{jiang2022thor,
     title = {Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers},
     author = {Jiang, Albert Q and Li, Wenda and Tworkowski, Szymon and Czechowski, Konrad and Odrzyg{\'o}{\'z}d{\'z}, Tomasz and Mi{\l}o{\'s}, Piotr and Wu, Yuhuai and Jamnik, Mateja},
     booktitle = {Conference on Neural Information Processing Systems,},
     year = {2022}
   }

2. NeurIPS

   Autoformalization with large language models

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

   2022

   Bib HTML PDF

   @article{wu2022autoformalization,
     title = {Autoformalization with large language models},
     author = {Wu, Yuhuai and Jiang, Albert Q and Li, Wenda and Rabe, Markus N and Staats, Charles and Jamnik, Mateja and Szegedy, Christian},
     booktitle = {Conference on Neural Information Processing Systems,},
     year = {2022}
   }

3. EM

   Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types

   Anthony Bordg, Lawrence Paulson, and Wenda Li

   Experimental Mathematics 2022

   Bib HTML PDF

   @article{bordg2022simple,
     title = {Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types},
     author = {Bordg, Anthony and Paulson, Lawrence and Li, Wenda},
     journal = {Experimental Mathematics},
     pages = {1--19},
     year = {2022},
     publisher = {Taylor \& Francis}
   }

4. AITP

   Learning Plausible and Useful Conjectures

   Albert Q. Jiang, Wenda Li, and Mateja Jamnik

   7th Conference on Artificial Intelligence and Theorem Proving 2022

   Bib

   @article{jiang2021lisb,
     title = {Learning Plausible and Useful Conjectures},
     author = {Jiang, Albert Q. and Li, Wenda and Jamnik, Mateja},
     year = {2022},
     journal = {7th Conference on Artificial Intelligence and Theorem Proving}
   }

2021

1. EM

   Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL

   Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence C Paulson

   Experimental Mathematics 2021

   Bib HTML PDF

   @article{koutsoukou2021irrationality,
     title = {Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL},
     author = {Koutsoukou-Argyraki, Angeliki and Li, Wenda and Paulson, Lawrence C},
     journal = {Experimental Mathematics},
     pages = {1--12},
     year = {2021},
     publisher = {Taylor \& Francis}
   }

2. ICML

   Lime: Learning inductive bias for primitives of mathematical reasoning

   Yuhuai Wu, Markus N Rabe, Wenda Li, and 3 more authors

   In International Conference on Machine Learning, 2021

   Bib PDF

   @inproceedings{wu2021lime,
     title = {Lime: Learning inductive bias for primitives of mathematical reasoning},
     author = {Wu, Yuhuai and Rabe, Markus N and Li, Wenda and Ba, Jimmy and Grosse, Roger B and Szegedy, Christian},
     booktitle = {International Conference on Machine Learning,},
     pages = {11251--11262},
     year = {2021},
     organization = {PMLR}
   }

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

4. AFP

   The Theorem of Three Circles

   Fox Thomson, and Wenda Li

   Archive of Formal Proofs, Aug 2021

   Bib HTML

   @article{Three_Circles-AFP,
     author = {Thomson, Fox and Li, Wenda},
     title = {The Theorem of Three Circles},
     journal = {Archive of Formal Proofs,},
     month = aug,
     year = {2021},
                 Formal proof development},
     issn = {2150-914x}
   }

5. AFP

   Grothendieck’s Schemes in Algebraic Geometry

   Anthony Bordg, Lawrence C. Paulson, and Wenda Li

   Archive of Formal Proofs, Mar 2021

   Bib HTML

   @article{Grothendieck_Schemes-AFP,
     author = {Bordg, Anthony and Paulson, Lawrence C. and Li, Wenda},
     title = {Grothendieck's Schemes in Algebraic Geometry},
     journal = {Archive of Formal Proofs,},
     month = mar,
     year = {2021},
                 Formal proof development},
     issn = {2150-914x}
   }

6. AITP

   LISA: Language models of ISAbelle proofs

   Albert Q. Jiang, Wenda Li, Jesse Michael Han, and 1 more author

   6th Conference on Artificial Intelligence and Theorem Proving Mar 2021

   Bib Code

   @article{jiang2021lisa,
     title = {LISA: Language models of ISAbelle proofs},
     author = {Jiang, Albert Q. and Li, Wenda and Han, Jesse Michael and Wu, Yuhuai},
     year = {2021},
     journal = {6th Conference on Artificial Intelligence and Theorem Proving}
   }

2020

1. JAR

   Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL

   Wenda Li, and Lawrence C Paulson

   Journal of Automated Reasoning Mar 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}
   }

2. AFP

   Irrationality Criteria for Series by Erdős and Straus

   Angeliki Koutsoukou-Argyraki, and Wenda Li

   Archive of Formal Proofs, May 2020

   Bib HTML

   @article{Irrational_Series_Erdos_Straus-AFP,
     author = {Koutsoukou-Argyraki, Angeliki and Li, Wenda},
     title = {Irrationality Criteria for Series by Erdős and Straus},
     journal = {Archive of Formal Proofs,},
     month = may,
     year = {2020},
                 Formal proof development},
     issn = {2150-914x}
   }

2019

1. CPP

   Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem

   Wenda Li, and Lawrence C Paulson

   In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, May 2019

   Bib HTML PDF Code

   @inproceedings{li2019counting,
     title = {Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem},
     author = {Li, Wenda and Paulson, Lawrence C},
     booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs,},
     pages = {52--64},
     year = {2019}
   }

2. JAR

   Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL

   Wenda Li, Grant Olney Passmore, and Lawrence C Paulson

   Journal of Automated Reasoning, May 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}
   }

3. Thesis

   Towards justifying computer algebra algorithms in Isabelle/HOL

   Wenda Li

   May 2019

   Bib HTML PDF

   @phdthesis{li2019towards,
     title = {Towards justifying computer algebra algorithms in Isabelle/HOL},
     author = {Li, Wenda},
     year = {2019},
     school = {University of Cambridge}
   }

4. AFP

   The Transcendence of Certain Infinite Series

   Angeliki Koutsoukou-Argyraki, and Wenda Li

   Archive of Formal Proofs, Mar 2019

   Bib HTML

   @article{Transcendence_Series_Hancl_Rucki-AFP,
     author = {Koutsoukou-Argyraki, Angeliki and Li, Wenda},
     title = {The Transcendence of Certain Infinite Series},
     journal = {Archive of Formal Proofs,},
     month = mar,
     year = {2019},
                 Formal proof development},
     issn = {2150-914x}
   }

2018

1. AFP

   Irrational Rapidly Convergent Series

   Angeliki Koutsoukou-Argyraki, and Wenda Li

   Archive of Formal Proofs, May 2018

   Bib HTML

   @article{Irrationality_J_Hancl-AFP,
     author = {Koutsoukou-Argyraki, Angeliki and Li, Wenda},
     title = {Irrational Rapidly Convergent Series},
     journal = {Archive of Formal Proofs,},
     month = may,
     year = {2018},
                 Formal proof development},
     issn = {2150-914x}
   }

2. AFP

   The Budan-Fourier Theorem and Counting Real Roots with Multiplicity

   Wenda Li

   Archive of Formal Proofs, Sep 2018

   Bib HTML

   @article{Budan_Fourier-AFP,
     author = {Li, Wenda},
     title = {The Budan-Fourier Theorem and Counting Real Roots with Multiplicity},
     journal = {Archive of Formal Proofs,},
     month = sep,
     year = {2018},
                 Formal proof development},
     issn = {2150-914x}
   }

2017

1. AFP

   Evaluate Winding Numbers through Cauchy Indices

   Wenda Li

   Archive of Formal Proofs, Oct 2017

   Bib HTML

   @article{Winding_Number_Eval-AFP,
     author = {Li, Wenda},
     title = {Evaluate Winding Numbers through Cauchy Indices},
     journal = {Archive of Formal Proofs,},
     month = oct,
     year = {2017},
                 Formal proof development},
     issn = {2150-914x}
   }

2. AFP

   Count the Number of Complex Roots

   Wenda Li

   Archive of Formal Proofs, Oct 2017

   Bib HTML

   @article{Count_Complex_Roots-AFP,
     author = {Li, Wenda},
     title = {Count the Number of Complex Roots},
     journal = {Archive of Formal Proofs,},
     month = oct,
     year = {2017},
                 Formal proof development},
     issn = {2150-914x}
   }

2016

1. ITP

   A formal proof of Cauchy’s residue theorem

   Wenda Li, and Lawrence C Paulson

   In International Conference on Interactive Theorem Proving, Oct 2016

   Bib PDF

   @inproceedings{li2016formal,
     title = {A formal proof of Cauchy’s residue theorem},
     author = {Li, Wenda and Paulson, Lawrence C},
     booktitle = {International Conference on Interactive Theorem Proving,},
     pages = {235--251},
     year = {2016},
     organization = {Springer}
   }

2. CPP

   A modular, efficient formalisation of real algebraic numbers

   Wenda Li, and Lawrence C Paulson

   In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Oct 2016

   Bib HTML PDF

   @inproceedings{li2016modular,
     title = {A modular, efficient formalisation of real algebraic numbers},
     author = {Li, Wenda and Paulson, Lawrence C},
     booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs,},
     pages = {66--75},
     year = {2016}
   }

2015

2014

1. Systems analysis of auxin transport in the Arabidopsis root apex

   Leah R Band, Darren M Wells, John A Fozard, and 8 more authors

   The Plant Cell, Oct 2014

   Bib HTML

   @article{band2014systems,
     title = {Systems analysis of auxin transport in the Arabidopsis root apex},
     author = {Band, Leah R and Wells, Darren M and Fozard, John A and Ghetiu, Teodor and French, Andrew P and Pound, Michael P and Wilson, Michael H and Yu, Lei and Li, Wenda and Hijazi, Hussein I and others},
     journal = {The Plant Cell,},
     volume = {26},
     number = {3},
     pages = {862--875},
     year = {2014},
     publisher = {American Society of Plant Biologists}
   }

2. AFP

   The Sturm-Tarski Theorem

   Wenda Li

   Archive of Formal Proofs, Sep 2014

   Bib HTML

   @article{Sturm_Tarski-AFP,
     author = {Li, Wenda},
     title = {The Sturm-Tarski Theorem},
     journal = {Archive of Formal Proofs,},
     month = sep,
     year = {2014},
                 Formal proof development},
     issn = {2150-914x}
   }

2013

1. AFP

   The Königsberg Bridge Problem and the Friendship Theorem

   Wenda Li

   Archive of Formal Proofs, Jul 2013

   Bib HTML

   @article{Koenigsberg_Friendship-AFP,
     author = {Li, Wenda},
     title = {The Königsberg Bridge Problem and the Friendship Theorem},
     journal = {Archive of Formal Proofs,},
     month = jul,
     year = {2013},
                 Formal proof development},
     issn = {2150-914x}
   }