  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.
