publications

2026

1. ICML

   Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models

   Joshua Ong Jun Leang, Yu Zhao, Mihaela Cătălina Stoian, and 3 more authors

   In International Conference on Machine Learning, 2026

   Bib HTML

   @inproceedings{leang2026order,
     title = {Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models},
     author = {Leang, Joshua Ong Jun and Zhao, Yu and Stoian, Mihaela C{\u{a}}t{\u{a}}lina and Li, Wenda and Cohen, Shay B. and Giunchiglia, Eleonora},
     year = {2026},
     archiveprefix = {arXiv},
     primaryclass = {cs.CL},
     booktitle = {International Conference on Machine Learning},
   }

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

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

4. ACL Findings

   PiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains

   Joshua Ong Jun Leang, Zheng Zhao, Aryo Pradipta Gema, and 7 more authors

   In Findings of the Association for Computational Linguistics, 2026

   Bib HTML

   @inproceedings{leang2025picsarprobabilisticconfidenceselection,
     title = {PiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains},
     author = {Leang, Joshua Ong Jun and Zhao, Zheng and Gema, Aryo Pradipta and Yang, Sohee and Kwan, Wai-Chung and He, Xuanli and Li, Wenda and Minervini, Pasquale and Giunchiglia, Eleonora and Cohen, Shay B.},
     year = {2026},
     archiveprefix = {arXiv},
     primaryclass = {cs.CL},
     booktitle = {Findings of the Association for Computational Linguistics},
   }

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

2025

1. ACL

   Theorem Prover as a Judge for Synthetic Data Generation

   Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and 1 more author

   In Association for Computational Linguistics, 2025

   Bib HTML

   @inproceedings{leang2025theoremproverjudgesynthetic,
     title = {Theorem Prover as a Judge for Synthetic Data Generation},
     author = {Leang, Joshua Ong Jun and Hong, Giwon and Li, Wenda and Cohen, Shay B.},
     year = {2025},
     archiveprefix = {arXiv},
     primaryclass = {cs.AI},
     booktitle = {Association for Computational Linguistics},
   }

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

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

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

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 Qiaochu Jiang, Wenda Li, and 4 more authors

   Advances in Neural Information Processing Systems, 2022

   Bib PDF

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

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

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

   https://isa-afp.org/entries/Three_Circles.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Three_Circles.html},
                 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

   https://isa-afp.org/entries/Grothendieck_Schemes.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Grothendieck_Schemes.html},
                 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, 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, 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

   https://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Irrational_Series_Erdos_Straus.html},
                 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,, 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,, 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

   University of Cambridge, 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

   https://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html},
                 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

   https://isa-afp.org/entries/Irrationality_J_Hancl.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Irrationality_J_Hancl.html},
                 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

   https://isa-afp.org/entries/Budan_Fourier.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Budan_Fourier.html},
                 Formal proof development},
     issn = {2150-914x}
   }

2017

1. AFP

   Evaluate Winding Numbers through Cauchy Indices

   Wenda Li

   Archive of Formal Proofs, Oct 2017

   https://isa-afp.org/entries/Winding_Number_Eval.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Winding_Number_Eval.html},
                 Formal proof development},
     issn = {2150-914x}
   }

2. AFP

   Count the Number of Complex Roots

   Wenda Li

   Archive of Formal Proofs, Oct 2017

   https://isa-afp.org/entries/Count_Complex_Roots.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Count_Complex_Roots.html},
                 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,, 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,, 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}
   }

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

   https://isa-afp.org/entries/Sturm_Tarski.html, Formal proof development

   Bib HTML

   @article{Sturm_Tarski-AFP,
     author = {Li, Wenda},
     title = {The Sturm-Tarski Theorem},
     journal = {Archive of Formal Proofs},
     month = sep,
     year = {2014},
     note = {\url{https://isa-afp.org/entries/Sturm_Tarski.html},
                 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

   https://isa-afp.org/entries/Koenigsberg_Friendship.html, Formal proof development

   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},
     note = {\url{https://isa-afp.org/entries/Koenigsberg_Friendship.html},
                 Formal proof development},
     issn = {2150-914x}
   }