Formalization and Implementation of Algebraic Methods in Geometry

TL;DR

This paper discusses the formalization and implementation of algebraic methods like Wu's method and Groebner bases for geometry theorem proving, aiming to enhance educational tools and bridge gaps between algebraic and synthetic geometry.

Contribution

It introduces a formal verification within Isabelle/HOL and a new open-source Java implementation of algebraic methods for geometry theorem proving.

Findings

Formal verification of algebraic methods in Isabelle/HOL

Development of an open-source Java implementation

Integration of algebraic methods with educational geometry tools

Abstract

We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the algebraic methods within Isabelle/HOL proof assistant and development of a new, open-source Java implementation of the algebraic methods. The project should fill-in some gaps still existing in this area (e.g., the lack of formal links between algebraic methods and synthetic geometry and the lack of self-contained implementations of algebraic methods suitable for integration with dynamic geometry tools) and should enable new applications of theorem proving in education.