Computer-Assisted Theorem Proving in Synthetic Geometry

Computer-assisted proof in mathematics has been underway since the pioneering times of computers in the 1950s. Starting from early systems with very limited capability, Computer-Assisted Theorem Proving has evolved to demonstrate theorems never proved before by humans [156] and assist with monumental efforts spanning several man-years [116]. In this endeavour, geometry plays an important part, just as it has throughout the history of mathematics. This is due to its pervasive role: it is a paradigmatic form of reasoning, with applications to education, mathematical and physical research, but also to many applied areas such as robotics, computer vision, and CAD [48]. Moreover, many of the search techniques and other algorithmic features developed for geometric reasoning have influenced other areas of artificial intelligence.