A Machine Proof System of Point Geometry Based on Coq

Abstract

An important development in geometric algebra in recent years is the new system known as point geometry, which treats points as direct objects of operations and considerably simplifies the process of geometric reasoning. In this paper, we provide a complete formal description of the point geometry theory architecture and give a rigorous and reliable formal verification of the point geometry theory based on the theorem prover Coq. Simultaneously, a series of tactics are also designed to assist in the proof of geometric propositions. Based on the theoretical architecture and proof tactics, a universal and scalable interactive point geometry machine proof system, PointGeo, is built. In this system, any arbitrary point-geometry-solvable geometric statement may be proven, along with readable information about the solution’s procedure. Additionally, users may augment the rule base by adding trustworthy rules as needed for certain issues. The implementation of the system expands the library of Coq resources on geometric algebra, which will become a significant research foundation for the fields of geometric algebra, computer science, mathematics education, and other related fields.

Keywords

• point geometry
• formal method
• interact theorem proving
• Coq
• machine proof