This paper gives a brief overview of FG, a formal system for doing Euclidean geometry whose basic syntactic elements are geometric diagrams, and which has been implimentented as the computer system CDEG. The computational complexity of determining whether or not a given diagram is satisfiable is also briefly discussed. 1 A Diagrammatic Formal System To begin with, consider Euclid’s first proposition, which says that an equilateral triangle can be constructed on any given base. While Euclid wrote his proof in Greek with