Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux
TL;DR
This work tackles the challenge of interleaving conjecturing and proving in synthetic Euclidean geometry by introducing a uniform framework that completes incomplete conjectures and proofs via abducts (missing assumptions), deducts (partially specified goals), and hints (partial proofs) within coherent logic. The method extends the Larus system to operate with constraint solving, enabling machine-checkable and human-readable proofs, and it demonstrates the approach on Varignon-related problems, showing abducts can recover nontrivial assumptions, deducts can guide goal formation, and hints can accelerate proof reconstruction. The approach is limited to coherent logic (no function symbols) and relatively short proofs, but it paves the way for transferring informal geometric knowledge to proof assistants and for integrating with language models to support automatic formalization and didactic exploration. Overall, the framework provides a flexible, uniform, and practical path to automate and explain partially specified geometric reasoning in a way that supports education, research, and verification.
Abstract
Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.