Document Open Access Logo

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Authors Aeacus Sheng , Wenda Li , Paul B. Jackson

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.32.pdf
  • Filesize: 0.73 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Isabelle/HOL
  • Real root isolation
  • Descartes' rule of signs

Metrics

Abstract

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.

Cite As Get BibTex

Aeacus Sheng, Wenda Li, and Paul B. Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 32:1-32:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.32

Author Details

Aeacus Sheng
  • University of Edinburgh, UK
Wenda Li
  • University of Edinburgh, UK
Paul B. Jackson
  • University of Edinburgh, UK

Supplementary Materials

References

  1. Victor Aladjev. Computer algebra system Maple: A new software library. In Peter M. A. Sloot, David Abramson, Alexander V. Bogdanov, Jack J. Dongarra, Albert Y. Zomaya, and Yuriy E. Gorbachev, editors, Computational Science - ICCS 2003, pages 711-717, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44860-8_73.
  2. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics, 10. Springer Berlin Heidelberg, Berlin, Heidelberg, 2nd edition, 2006. URL: https://doi.org/10.1007/3-540-33099-2.
  3. Yves Bertot, Frédérique Guilhot, and Assia Mahboubi. A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science, 21(4):731-761, 2011. URL: https://doi.org/10.1017/S0960129511000090.
  4. Dario A. Bini and Leonardo Robol. Solving secular and polynomial equations: A multiprecision algorithm. Journal of Computational and Applied Mathematics, 272:276-292, 2014. URL: https://doi.org/10.1016/j.cam.2013.04.037.
  5. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. In Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), CADE'11, pages 116-130, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-22438-6_11.
  6. George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report. ACM SIGSAM Bulletin, 8(3):80-90, August 1974. URL: https://doi.org/10.1145/1086837.1086852.
  7. George E. Collins and Werner Krandick. An efficient algorithm for infallible polynomial complex root isolation. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC '92), pages 189-194. ACM, 1992. URL: https://doi.org/10.1145/143242.143286.
  8. Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada. A formalization of the Berlekamp-Zassenhaus factorization algorithm. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 17-29, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018617.
  9. Manuel Eberl. A decision procedure for univariate real polynomials in Isabelle/HOL. In Proceedings of the 4th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2015). ACM, 2015. URL: https://doi.org/10.1145/2676724.2693166.
  10. Manuel Eberl. Descartes' rule of signs. Archive of Formal Proofs, December 2015. URL: https://www.isa-afp.org/entries/Descartes_Sign_Rule.shtml.
  11. Manuel Eberl and Peter Lammich. Verifying an efficient algorithm for computing Bernoulli numbers. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:19, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.35.
  12. Alperen Ergür, Josué Tonelli-Cueto, and Elias Tsigaridas. Beyond worst-case analysis for root isolation algorithms. In Proceedings of the 2022 International Symposium on Symbolic and Algebraic Computation, ISSAC '22, pages 139-148, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3476446.3535475.
  13. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pages 103-117, 2010. 10th International Symposium on Functional and Logic Programming, FLOPS 2010 ; Conference date: 19-04-2010 Through 21-04-2010. URL: https://doi.org/10.1007/978-3-642-12251-4_9.
  14. Michael Hemmer, Elias P. Tsigaridas, Zafeirakis Zafeirakopoulos, Ioannis Z. Emiris, Menelaos I. Karavelas, and Bernard Mourrain. Experimental evaluation and cross-benchmarking of univariate real solvers. In Proceedings of the 2009 Conference on Symbolic Numeric Computation, SNC '09, pages 45-54, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1577190.1577202.
  15. J. R. Johnson. Algorithms for polynomial real root isolation. In Bob F. Caviness and Jeremy R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 269-299, Vienna, 1998. Springer Vienna. URL: https://doi.org/10.1007/978-3-7091-9459-1_13.
  16. Sebastiaan Joosten, René Thiemann, and Akihisa Yamada. A verified implementation of algebraic numbers in Isabelle/HOL. Journal of Automated Reasoning, 64, March 2020. URL: https://doi.org/10.1007/s10817-018-09504-w.
  17. Alexander Kobel, Fabrice Rouillier, and Michael Sagraloff. Computing real roots of real polynomials ... and now for real! In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 2016), pages 303-310. ACM, 2016. URL: https://doi.org/10.1145/2930889.2930937.
  18. Alexander Krauss. Defining Recursive Functions in Isabelle/HOL. Technische Universität München, 2012. Part of the official Isabelle documentation distribution. Google Scholar
  19. Peter Lammich. Generating verified LLVM from Isabelle/HOL. In ITP 2019: Interactive Theorem Proving, June 2019. Interactive Theorem Proving, ITP 2019 ; Conference date: 08-09-2019 Through 13-09-2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.22.
  20. Wenda Li. The Budan-Fourier theorem and counting real roots with multiplicity. Archive of Formal Proofs, September 2018. URL: https://www.isa-afp.org/entries/Budan_Fourier.html.
  21. Wenda Li, Grant Olney Passmore, and Lawrence C Paulson. Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Journal of Automated Reasoning, 62(1):69-91, 2019. URL: https://doi.org/10.1007/s10817-017-9424-6.
  22. Wenda Li and Lawrence C. Paulson. Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '19), pages 52-64. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294092.
  23. Anthony Narkawicz, César Muñoz, and Aaron Dutle. Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. Journal of Automated Reasoning, 54(4):285-326, 2015. URL: https://doi.org/10.1007/s10817-015-9320-x.
  24. Anthony Joseph Narkawicz, Cesar Munoz, and Aaron M. Dutle. A decision procedure for univariate polynomial systems based on root counting and interval subdivision. Journal of Formalized Reasoning, 11(1):19-41, January 2018. URL: https://doi.org/10.6092/issn.1972-5787/8212.
  25. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  26. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, IWIL 2010. The 8th International Workshop on the Implementation of Logics, volume 2 of EPiC Series in Computing, pages 1-11. EasyChair, 2012. URL: https://doi.org/10.29007/36dt.
  27. Michael Sagraloff. When Newton meets Descartes: A simple and fast algorithm to isolate the real roots of a polynomial. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 2012), pages 297-304. ACM, 2012. URL: https://doi.org/10.1145/2442829.2442872.
  28. Aeacus Sheng. Dsc. Software, (visited on 2026-07-06). URL: https://github.com/Aeacu2/Dsc
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26768
  29. The Mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pages 367-381. Association for Computing Machinery, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  30. The Sage Developers. SageMath, the Sage Mathematics Software System (Version 10.8), 2025. https://www.sagemath.org. Google Scholar
  31. René Thiemann and Akihisa Yamada. Polynomial factorization. Archive of Formal Proofs, January 2016. URL: https://www.isa-afp.org/entries/Polynomial_Factorization.shtml.
  32. Fox Thomson and Wenda Li. The theorem of three circles. Archive of Formal Proofs, August 2021. URL: https://www.isa-afp.org/entries/Three_Circles.html.
  33. Freek Wiedijk. Formalizing 100 theorems. https://www.cs.ru.nl/~freek/100/, 2024. Accessed: February 14, 2026.
  34. Z3 source: Real root isolation via Descartes' rule of signs. https://github.com/Z3Prover/z3/blob/43791ebf2abeb91fbe78656dd122c0f28b61098c/src/math/polynomial/upolynomial.cpp#L2506-L2509, 2026. Z3 4.17.0.0, commit 43791eb.
  35. Julianna Zsidó. Theorem of three circles in Coq. Journal of Automated Reasoning, December 2013. 25 pages, 5 figures. URL: https://doi.org/10.1007/s10817-013-9299-0.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact