@misc{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={2024},eprint={2412.16075},archiveprefix={arXiv},primaryclass={cs.AI},}
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
@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
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
@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,}}
arXiv
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Huajian Xin, Daya Guo, Zhihong Shao, and 6 more authors
@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.'}}
NeurIPS
Proving Theorems Recursively
Haiming Wang, Huajian Xin, Zhengying Liu, and 8 more authors
In Conference on Neural Information Processing Systems,, 2024
@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,}}
NeurIPS
End-to-End Ontology Learning with Large Language Models
Andy Lo, Albert Q. Jiang, Wenda Li, and 1 more author
@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,}}
@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
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
@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}}
PNAS
Evaluating Language Models for Mathematics through Interactions
Katherine M. Collins, Albert Q. Jiang, Simon Frieder, and 11 more authors
@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.},}
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
@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
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
@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
NeurIPS
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Albert Q Jiang, Wenda Li, Szymon Tworkowski, and 5 more authors
@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}}
NeurIPS
Autoformalization with large language models
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, and 4 more authors
Advances in Neural Information Processing Systems, 2022
@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},}
EM
Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
@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}}
AITP
Learning Plausible and Useful Conjectures
Albert Q. Jiang, Wenda Li, and Mateja Jamnik
7th Conference on Artificial Intelligence and Theorem Proving, 2022
@article{jiang2021conjecture,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
EM
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence C Paulson
@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}}
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
@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}}
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
@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},}
AFP
The Theorem of Three Circles
Fox Thomson, and Wenda Li
Archive of Formal Proofs,, Aug 2021
\urlhttps://isa-afp.org/entries/Three_Circles.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Three_Circles.html},
Formal proof development},issn={2150-914x}}
AFP
Grothendieck’s Schemes in Algebraic Geometry
Anthony Bordg, Lawrence C. Paulson, and Wenda Li
Archive of Formal Proofs,, Mar 2021
\urlhttps://isa-afp.org/entries/Grothendieck_Schemes.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Grothendieck_Schemes.html},
Formal proof development},issn={2150-914x}}
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
@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
JAR
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
@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}}
AFP
Irrationality Criteria for Series by Erdős and Straus
Angeliki Koutsoukou-Argyraki, and Wenda Li
Archive of Formal Proofs,, May 2020
\urlhttps://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html},
Formal proof development},issn={2150-914x}}
2019
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
@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}}
JAR
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
Wenda Li, Grant Olney Passmore, and Lawrence C Paulson
@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}}
Thesis
Towards justifying computer algebra algorithms in Isabelle/HOL
@phdthesis{li2019towards,title={Towards justifying computer algebra algorithms in Isabelle/HOL},author={Li, Wenda},year={2019},school={University of Cambridge}}
AFP
The Transcendence of Certain Infinite Series
Angeliki Koutsoukou-Argyraki, and Wenda Li
Archive of Formal Proofs,, Mar 2019
\urlhttps://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html},
Formal proof development},issn={2150-914x}}
2018
AFP
Irrational Rapidly Convergent Series
Angeliki Koutsoukou-Argyraki, and Wenda Li
Archive of Formal Proofs,, May 2018
\urlhttps://isa-afp.org/entries/Irrationality_J_Hancl.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Budan_Fourier.html},
Formal proof development},issn={2150-914x}}
2017
AFP
Evaluate Winding Numbers through Cauchy Indices
Wenda Li
Archive of Formal Proofs,, Oct 2017
\urlhttps://isa-afp.org/entries/Winding_Number_Eval.html, Formal proof development
@article{Count_Complex_Roots-AFP,author={Li, Wenda},title={Count the Number of Complex Roots},journal={Archive of Formal Proofs,},month=oct,year={2017},note={\url{https://isa-afp.org/entries/Count_Complex_Roots.html},
Formal proof development},issn={2150-914x}}
2016
ITP
A formal proof of Cauchy’s residue theorem
Wenda Li, and Lawrence C Paulson
In International Conference on Interactive Theorem Proving,, Oct 2016
@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}}
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
@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}}
2014
Systems analysis of auxin transport in the Arabidopsis root apex
Leah R Band, Darren M Wells, John A Fozard, and 8 more authors
@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}}
AFP
The Sturm-Tarski Theorem
Wenda Li
Archive of Formal Proofs,, Sep 2014
\urlhttps://isa-afp.org/entries/Sturm_Tarski.html, Formal proof development
@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},note={\url{https://isa-afp.org/entries/Koenigsberg_Friendship.html},
Formal proof development},issn={2150-914x}}