A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016
We investigated synthetic geometry and propositions from Euclid's Elements using constructive mathematics and utilizing results from Beeson, Tarski, Hilbert, and Euclid. See Constructive Geometry in Nuprl.