Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

Automated theorem provers take as input the formal statement of a conjecture in a theory described by axioms and lemmas, and try to generate a proof or a counter-example for this conjecture. In the field of geometry, several efficient automated theorem proving approaches have been developed, including algebraic ones such as Wu's method, Gröbner bases method, and semi-synthetic methods such as the area method. In these approaches, typically, the conjecture and the axioms being considered are fixed. However, in mathematical practice, in the context of education and also in mathematical research, the conjecturing and proving activities are not separated but interleaved. The practitioner may try to prove a statement which is valid only assuming some implicit or unknown assumptions, while the list of lemmas and theorem which can be used may not be complete.