ABSTRACT
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 and assist with monumental efforts spanning several man-years. Geometric theorems can be proved not only by dedicated systems but also by general ones, typically by theorem provers for first order logic or some of its fragments such as Coherent logic. Proof assistants are designed for checking proofs generated by the user, but it is also possible to check proofs generated by automated theorem provers. The latter can be used to prove theorems wholesale or, at a smaller scale, to automate parts of proofs which are produced interactively. In the synthetic approach, the geometry theory is built from axioms, with non-logical symbols corresponding to geometric predicates, and sorts corresponding to geometric objects.
