Wenda Li

23 papers A* 2B 4Journal 16Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification.
Commun. ACM
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, Dawn Song
2025 J jnl
Complex Lattices, Elliptic Functions, and the Modular Group.
Arch. Formal Proofs
Manuel Eberl, Anthony Bordg, Wenda Li, Lawrence C. Paulson
2025 J jnl
Dedekind Sums.
Arch. Formal Proofs
Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li
2025 — conf
Position: Formal Mathematical Reasoning - A New Frontier in AI.
ICML (Position Papers)
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, Dawn Song
2024 J jnl
Formal Mathematical Reasoning: A New Frontier in AI.
CoRR
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, Dawn Song
2024 B conf
Formalising Half of a Graduate Textbook on Number Theory (Short Paper).
ITP
Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li
2024 A* conf
Subgoal-based Demonstration Learning for Formal Theorem Proving.
ICML
Xueliang Zhao, Wenda Li, Lingpeng Kong
2023 J jnl
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving.
CoRR
Xueliang Zhao, Wenda Li, Lingpeng Kong
2022 J jnl
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.
Exp. Math.
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
2022 J jnl
Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types.
Exp. Math.
Anthony Bordg, Lawrence C. Paulson, Wenda Li
2021 J jnl
Grothendieck's Schemes in Algebraic Geometry.
Arch. Formal Proofs
Anthony Bordg, Lawrence C. Paulson, Wenda Li
2021 J jnl
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.
CoRR
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
2021 A* conf
IsarStep: a Benchmark for High-level Mathematical Reasoning.
ICLR
Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
2021 J jnl
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types.
CoRR
Anthony Bordg, Lawrence C. Paulson, Wenda Li
2020 J jnl
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.
J. Autom. Reason.
Wenda Li, Lawrence C. Paulson
2020 J jnl
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs.
CoRR
Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
2019 B conf
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem.
CPP
Wenda Li, Lawrence C. Paulson
2019 J jnl
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL.
J. Autom. Reason.
Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
2018 J jnl
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem.
CoRR
Wenda Li, Lawrence C. Paulson
2018 J jnl
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL.
CoRR
Wenda Li, Lawrence C. Paulson
2016 B conf
A Formal Proof of Cauchy's Residue Theorem.
ITP
Wenda Li, Lawrence C. Paulson
2016 B conf
A modular, efficient formalisation of real algebraic numbers.
CPP
Wenda Li, Lawrence C. Paulson
2015 J jnl
A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.
CoRR
Wenda Li, Grant Olney Passmore, Lawrence C. Paulson