A Certified Version of Clark Kimberling's Encyclopedia of Triangle Centers

About

Goal

The goal of this project is to provide a certified version of Clark Kimberling's Encyclopedia of Triangle Centers (ETC).

Motivations

There are many results in the Encyclopedia of Triangle Centers but most are stated without proof. Even if the proofs were provided it would be infeasable for a human to check by hand all the properties.

Most of the results have been validated by computations using computer algebra systems but ETC does not provide the computation scripts and typos may have been introduced in the process (see for example message #2225 on ADGEOM mailing list).

Approach

For each point we display the coordinates we have used for the computations and proofs.
For each property we attach a level of certification:

What is a proof assistant ?

A proof assistant is a software which allow to state mathematical properties and verify their proof. It is mainly interactive i.e. the proof is described by the user using a formal language. For some simple theories it is possible to automate some proofs. In this project we use the Coq proof assistant.

How Coq proofs are constructed ?

Many properties displayed in ETC can be reduced to a test to know if some equality between two expressions holds. If these expressions are polynomials then it can be solved by expanding the polynomials and checking if they are syntically the same. If one proves that this process is correct then you have a proof generator for equality of polynomials. This is roughly what the ring tactic of Coq does. We use mainly this tactic together with some heuristic to deal with square roots. For example if you want to test if three points are collinear you can used the following lemma:
 Lemma col_chara : forall A B C,  col A B C <->
   X(A)*Y(B)*Z(C) + Y(A)*Z(B)*X(C) + Z(A)*X(B)*Y(C)
 - Z(A)*Y(B)*X(C) - Y(A)*X(B)*Z(C) - X(A)*Z(B)*Y(C) = 0.
   

What is the difference between having a Coq proof and CAS computation ?

When you use a result displayed in the encyclopedia you need to trust several things.
By using a proof assistant we try to reduce the quantity of code that you need to trust.
Moreover, we hope that in the future we can extend the properties we can prove. For that, we can use a mix of automatic proofs by computations or interactive proofs performed by a human being. We also hope that the language of Coq could be a standard language in the geometry community to exchange statement without the risk of any missunderstanding.