Formal Verification of Completeness Theorem in Grundlagen der Geometrie

Hilbert’s Grundlagen der Geometrie remains a pivotal work in formal proof and modern mathematics, influencing geometric reasoning. This paper meticulously formalizes the continuity axioms and completeness theorem from Grundlagen der Geometrie using the Coq proof assistant. The continuity axioms, more intricate than Hilbert’s others, involve a complex logical structure due to the introduction of natural numbers and infinite sets. Leveraging Coq’s Calculus of Inductive Construction (CIC), we systematically formalize Hilbert’s first three groups of axioms. Building on this foundation, we formalize the continuity axioms by constructing mappings between points. This approach allows us to avoid introducing natural numbers and infinite sets. And it is extended to verify the completeness theorem, maintaining consistency with Hilbert’s logic and striving for the readable proofs. The paper demonstrates Coq’s effectiveness in rigorously verifying mathemathical theorems, enhancing the reliability of mathematical reasoning. The contribution significantly advances the broader endeavor to establish a robust foundation for formalized mathematical proofs, bridging the gap between classical geometric intuition and modern formal methods.