In a recent joint paper with Jeremy Avigad and John Mumma (forthcoming in the Review of Symbolic Logic, preprint available at the arXiv), we devise a formal system that is intended to faithfully capture the notion of Euclidean geometric proofs. Specifically, is meant to be a formal counterpart to Books I through [...]