Mechanical theorem proving in geometry is often viewed as one of the most successful areas of automated reasoning since many non-trivial geometric proofs can be produced automatically. The area has been studied intensively over the past 25 years and a wide array of sophisticated algebraic approaches (amongst others) have been developed to produce fully automatic, though often unreadable, proofs.
In this talk, however, I shall concentrate on the recent, growing interest for interactive theorem proving in the area, where automation, though important, has to be balanced against issues such as proof readability. In particular, I will highlight some recent work on formalizing geometry in interactive systems such as Isabelle/HOL and describe how it can be used, together with other mathematical theories, to reason formally about areas ranging from 17th century Newtonian physics to collision avoidance in aircraft trajectories.