Wenda Li

According to our database, Wenda Li authored at least 15 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Formalising Half of a Graduate Textbook on Number Theory (Formal Proof Development).

Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li

Dataset, June, 2024

Formalising Half of a Graduate Textbook on Number Theory (Short Paper).

Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Subgoal-based Demonstration Learning for Formal Theorem Proving.

Xueliang Zhao, Wenda Li, Lingpeng Kong

Proceedings of the Forty-first International Conference on Machine Learning, 2024

2023

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

Xueliang Zhao, Wenda Li, Lingpeng Kong

CoRR, 2023

2022

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.

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

Exp. Math., 2022

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

Anthony Bordg, Lawrence C. Paulson, Wenda Li

Exp. Math., 2022

2021

Grothendieck's Schemes in Algebraic Geometry.

Anthony Bordg, Lawrence C. Paulson, Wenda Li

Arch. Formal Proofs, 2021

IsarStep: a Benchmark for High-level Mathematical Reasoning.

Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson

Proceedings of the 9th International Conference on Learning Representations, 2021

2020

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

Wenda Li, Lawrence C. Paulson

J. Autom. Reason., 2020

Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs.

Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson

CoRR, 2020

2019

Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL.

Wenda Li, Grant Olney Passmore, Lawrence C. Paulson

J. Autom. Reason., 2019

Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem.

Wenda Li, Lawrence C. Paulson

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

2016

A Formal Proof of Cauchy's Residue Theorem.

Wenda Li, Lawrence C. Paulson

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

A modular, efficient formalisation of real algebraic numbers.

Wenda Li, Lawrence C. Paulson

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

2015

A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.

Wenda Li, Grant Olney Passmore, Lawrence C. Paulson

CoRR, 2015