# On Constructive-Deductive Method For Plane Euclidean Geometry

## TL;DR

This paper formalizes a constructive-deductive approach to plane Euclidean geometry within Coq, combining postulates for geometric constructions and axioms for properties of figures, offering a constructive alternative to Hilbert's system.

## Contribution

It introduces a formalized constructive-deductive system for Euclidean geometry in Coq, integrating elementary constructions and properties as a novel framework.

## Key findings

- Successfully formalized the system in Coq
- Provides a constructive version of Hilbert's axiomatization
- Enables formal proof development in Euclidean geometry

## Abstract

Constructive-deductive method for plane Euclidean geometry is proposed and formalized within Coq Proof Assistant. This method includes both postulates that describe elementary constructions by idealized geometric tools (pencil, straightedge and compass), and axioms that describes properties of basic geometric figures (points, lines, circles and triangles). The proposed system of postulates and axioms can be considered as a constructive version of the Hilbert's formalization of plane Euclidean geometry.

---
Source: https://tomesphere.com/paper/1903.05175