A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL. - Wenda Li 001; Grant Olney Passmore; Lawrence C. Paulson (CoRR, 2015)

A modular, efficient formalisation of real algebraic numbers. - Wenda Li 001; Lawrence C. Paulson (CPP, 2016)

A Formal Proof of Cauchy's Residue Theorem. - Wenda Li 001; Lawrence C. Paulson (ITP, 2016)

Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. - Wenda Li 001; Lawrence C. Paulson (CPP, 2019)

Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. - Wenda Li 001; Grant Olney Passmore; Lawrence C. Paulson (J. Autom. Reason., 2019)

Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. - Wenda Li 001; Lei Yu; Yuhuai Wu; Lawrence C. Paulson (CoRR, 2020)

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. - Wenda Li 001; Lawrence C. Paulson (J. Autom. Reason., 2020)

IsarStep: a Benchmark for High-level Mathematical Reasoning. - Wenda Li 001; Lei Yu; Yuhuai Wu; Lawrence C. Paulson (ICLR, 2021)

Grothendieck's Schemes in Algebraic Geometry. - Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (Arch. Formal Proofs, 2021)

Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types. - Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (Exp. Math., 2022)

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. - Angeliki Koutsoukou-Argyraki; Wenda Li 001; Lawrence C. Paulson (Exp. Math., 2022)

Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving. - Xueliang Zhao; Wenda Li 001; Lingpeng Kong (CoRR, 2023)

Subgoal-based Demonstration Learning for Formal Theorem Proving. - Xueliang Zhao; Wenda Li 001; Lingpeng Kong (ICML, 2024)

Formalising Half of a Graduate Textbook on Number Theory (Short Paper). - Manuel Eberl; Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (ITP, 2024)

Formalising Half of a Graduate Textbook on Number Theory (Formal Proof Development). - Manuel Eberl; Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (Zenodo, 2024)