Formalizing Algebrization of Geometry Statements

Abstract

For several decades, algebraic methods have been successfully used in automated deduction in geometry. Objects in Euclidean geometry and relations between them are expressed as polynomials, and algebraic methods (e.g., Gröbner bases) are used over such a set of polynomials. We describe a formalization of an algorithm in Isabelle/HOL that accepts a term representation of a geometry construction and returns a corresponding set of polynomials. Our further work involves using the method of Gröbner bases within Isabelle system on the generated polynomials, in order to implement a fully formally verified algebraic prover for geometry.