# * 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.

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.