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

From MaRDI portal
scientific article
Language Label Description Also known as
English
Towards a certified version of the encyclopedia of triangle centers
scientific article

    Statements

    Towards a certified version of the encyclopedia of triangle centers (English)
    0 references
    0 references
    0 references
    16 June 2016
    0 references
    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.
    0 references
    0 references
    triangle centers
    0 references
    geometry
    0 references
    formal proof
    0 references
    proof assistant
    0 references
    Coq
    0 references
    0 references