Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL

TL;DR

This paper introduces a proof procedure in Isabelle/HOL for univariate polynomial problems that leverages external algebraic tools with untrusted certificates, enabling efficient and correct verification of results.

Contribution

It combines external algebraic computations with formal proof verification in Isabelle/HOL, improving efficiency while maintaining correctness.

Findings

Significant performance improvements over previous methods.

Effective integration of external algebra systems with formal proof checking.

Demonstrated correctness and efficiency through experiments.

Abstract

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 decomposition. We follow the approach of untrusted certificates, separating solving from verifying: efficient external tools perform expensive real algebraic computations, producing evidence that is formally checked within Isabelle's logic. This allows us to exploit highly-tuned computer algebra systems like Mathematica to guide our procedure without impacting the correctness of its results. We present experiments demonstrating the efficacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.