New Opportunities for the Formal Proof of Computational Real Geometry?

TL;DR

This paper investigates the potential for formal, machine-verifiable proofs in real algebraic geometry, proposing a new algorithm that could improve the traceability and verifiability of computational results.

Contribution

It introduces a novel algorithm based on Cylindrical Algebraic Coverings aimed at enhancing formal proof capabilities in real algebraic geometry.

Findings

Proposes a new algorithm for satisfiability over the reals.

Suggests this algorithm offers better traceability for formal verification.

Highlights potential for more reliable machine-verifiable proofs.

Abstract

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.