Scholarlink

<p>The formalization of geometry theorems in a proof assistant such as Coq poses significant challenges, especially when dealing with higher dimensions. The complexity increases due to the numerous technical lemmas arising from the multitude of incidence relations. This paper explores the formalization of the <i>ordered geometry</i> derived from Hilbert’s <i>Foundations of Geometry</i>, a system that notably lacks any space order axioms. The proposed primary focus centers on a vital theorem: “A plane distinctly partitions space into two regions with specific properties”. Utilizing the Coq theorem prover, the authors establish order on both lines and planes. The proposed key contribution lies in extending these results to three-dimensional (3D) space. Remarkably, the work verifies the redundancy of additional space order axioms in Hilbert’s axiom system. This not only bridges a gap in existing research but also highlights the potency of computer proof assistants in ensuring mathematical rigor.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Formalizing Three-Dimensional Ordered Geometry in Coq: A Hilbert’s Perspective

  • 期刊论文

  • 发表日期：

    2026年1月16日

查看全文
  • Qimeng Zhang,
  • Wensheng Yu

摘要

The formalization of geometry theorems in a proof assistant such as Coq poses significant challenges, especially when dealing with higher dimensions. The complexity increases due to the numerous technical lemmas arising from the multitude of incidence relations. This paper explores the formalization of the ordered geometry derived from Hilbert’s Foundations of Geometry, a system that notably lacks any space order axioms. The proposed primary focus centers on a vital theorem: “A plane distinctly partitions space into two regions with specific properties”. Utilizing the Coq theorem prover, the authors establish order on both lines and planes. The proposed key contribution lies in extending these results to three-dimensional (3D) space. Remarkably, the work verifies the redundancy of additional space order axioms in Hilbert’s axiom system. This not only bridges a gap in existing research but also highlights the potency of computer proof assistants in ensuring mathematical rigor.