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

Abstract

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-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots.