ABSTRACT. Proving lemmas in synthetic geometry is an often time-consuming endeavour - many intermediate lemmas need to be proven before interesting results can be obtained. Automated theorem provers (ATP) made much progress in the recent years and can prove many of these intermediate lemmas automatically. The interactive theorem prover Elfe accepts mathematical texts written in fair English and verifies the text with the help of ATP. Geometrical texts can thereby easily be formalized in Elfe, leaving only the cornerstones of a proof to be derived by the user. This allows for teaching axiomatic geometry to students without prior experience in formal mathematics.