  The purpose of this paper is to explore the question "to what extent could we
produce formal, machine-verifiable, proofs in real algebraic geometry?" The
question has been asked before but as yet the leading algorithms for answering
such questions have not been formalised. We present a thesis that a new
algorithm for ascertaining satisfiability of formulae over the reals via
Cylindrical Algebraic Coverings [\'{A}brah\'{a}m, Davenport, England, Kremer,
\emph{Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a
Conflict Driver Search Using Cylindrical Algebraic Coverings}, 2020] might
provide trace and outputs that allow the results to be more susceptible to
machine verification than those of competing algorithms.
