This project aims to mechanise axiomatic geometry in Isabelle/HOL, providing a machine-checked formalisation of elementary Euclidean geometry based on Tarski-style axioms. The goal is to obtain a trustworthy, reusable foundation for geometric reasoning that supports both theoretical investigations and future mechanised mathematics.
Background
Axiomatic geometry studies geometric notions—such as points, betweenness, and congruence—by specifying a small set of primitive relations and axioms, rather than relying on coordinates or analytic representations. Tarski’s axioms are particularly attractive: they are first-order, minimalist, and known to be complete for Euclidean plane geometry. The metamathematical development by Schwabhäuser, Szmielew, and Tarski established deep results about consistency, completeness, and decidability, making this framework a canonical foundation for formalisation.
Scope
The project will encode Tarski’s axioms in Isabelle/HOL, define the core geometric relations, and mechanise key derived theorems (e.g. properties of betweenness, congruence, and basic constructions). The design will be informed by existing successful formal developments, in particular the Mizar formalisation of Tarski’s geometry, while adapting definitions and proof structure to Isabelle’s higher-order logic and proof automation. Emphasis will be placed on clarity, modularity, and proof reuse.
Expected Outcomes
The result will be a well-documented Isabelle/HOL theory of axiomatic Euclidean geometry, suitable as a foundation for further work in formal geometry, automated reasoning, and the integration of geometric arguments into larger verified systems. Ideally, the Isabelle/HOL development is ready for submission for the Archive of Formal Proofs.
References.
- Tarski’s Geometry and the Euclidean Plane in Mizar.
- W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983.