The "party line" of 20th-century logic generally held that Euclidean plane geometry did not enjoy a truly rigorous foundation until the creation of formal systems like those of Hilbert or Tarski. Until then, it was held, treatments such as Euclid's, with its diagrammatic methods of proof, suffered from an inappropriate reliance on intuition.

As Manders has pointed out, such a viewpoint sits in contradistinction to the fact that geometric practice was stable for millenia, and that Euclid was considered a paragon of mathematical rigor in that period. More than that, Manders has argued that the disparaging view of Euclidean proof is simply unwarranted. Avigad, Mumma and I have set about bolstering Manders' claim by crafting a straightforward, faithful formalization of the methods of Euclidean proof.

The resulting system E can be proven sound and complete for a semantics of ruler-and-compass constructions; and in proving this fact we find that E is not so distant from systems like Tarski's after all.