Towards a certified version of the encyclopedia of triangle centers (Q294378)

A triangle center of a triangle \(ABC\) is a point with trilinear coordinates \[ f(a, b, c) : f(b, c, a) : f(c, a, b) \] where \(a, b, c\) denote the side lengths of the triangle \(ABC\) and \(f\) is a homogeneous function with \(f(a, b, c) = f(a, c, b)\). Well-known examples of triangle centers are the center of gravity, the circumcenter, and the orthocenter of a triangle. The Encyclopedia of Triangle Centers (ETC) contains definitions and many properties of more than 7000 triangle centers. According to the authors, most properties in ETC are given without proof nor reference. The article presents an effort towards creating a certified version of ETC that provides formal proofs for the properties of the triangle centers. The authors describe how they use the interactive theorem prover Coq to formalize the definitions and constructions of triangle centers and some of their properties. Since parsing the properties given in ETC appears to be very challenging, the authors instead automatically generate conjectures about collinearity of triangle centers and transformations between triangle centers that can be automatically checked using Coq. For their Certified Encyclopedia of Triangle Centers (CETC), the authors thus managed to provide formal proofs for almost 80000 properties of 6000 triangle centers.