2026-07-22T22:17:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27006 2026-07-16T09:49:34Z ddc:004 open_access

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper) Sheng, Aeacus Li, Wenda Jackson, Paul B. Isabelle/HOL Real root isolation Descartes' rule of signs Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes' rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm's theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step towards efficient verified real root isolation by formally verifying two simple algorithms based on Descartes' rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms, present formal proofs of termination, soundness, and completeness, and discuss our code-generation efforts. Brief experiments show promising performance improvements over existing formally verified algorithms in Isabelle/HOL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aeacus Sheng and Wenda Li and Paul B. Jackson 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.32 urn:nbn:de:0030-drops-270068 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.32 eng https://creativecommons.org/licenses/by/4.0/legalcode