Skip to main content
PRL Project

Implementing Euclid's Straightedge and Compass Constructions in Type Theory

by Ariel Kellison, Mark Bickford, Robert L. Constable
2018


Constructions are central to the methodology of geometry presented
in the Elements. This theory therefore poses a unique challenge to those
concerned with the practice of constructive mathematics: can the Elements be
faithfully captured in a modern constructive framework? In this paper, we
outline our implementation of Euclidean geometry based on straightedge and
compass constructions in the intuitionistic type theory of the Nuprl proof assistant.
A result of our intuitionistic treatment of Euclidean geometry is a proof
of the second proposition from Book I of the Elements in its full generality;
a result that differs from other formally constructive accounts of Euclidean
geometry. Our formalization of the straightedge and compass utilizes a
predicate for orientation, which enables a concise and intuitive expression of
Euclid’s constructions.