43 citations · 151 across the 29 of their papers we have counts for
5 papers · 1 filter
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research…
IsarStep: a Benchmark for High-level Mathematical Reasoning
Wenda Li, Lei Yu, Yuhuai Wu +1
A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical…
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li, Lawrence C. Paulson
Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-count…
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL
Wenda Li, Lawrence C. Paulson
In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We…
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
We present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decompositi…