On the proof of the theorems of foundations of geometry using Isabelle/Hol

Abstract

Isabelle/HOL is a generic proof assistant. Using Isabelle/HOL requires insight into procedures as well as into the concepts involved. In addition, how a computer manages procedures can affect mathematical concepts. Use of Isabelle/HOL can correct a current weakness in mathematical studies. The advantage of the theorem proving support system represented by Isabelle/HOL is that it mechanically guarantees the “correctness” of both human-written programs and mathematical proofs. It can allow us to clearly understand mathematical concepts and can minimize the burden of operation opportunities. However, in order to take advantage of its high versatility and reliability, the problem that all certification procedures must be clearly formalized when creating certification must be overcome. “Foundations of Geometry” is a book on mathematics written by Hilbert in 1899. The book is famous as the most rigorous study of the axiom system of Euclidean geometry by axioms and formalism. When we tried to implement Hilbert’s axioms in Isabelle/HOL, the proofs based on human cognition hindered the implementation. The purpose of this paper is “correctly” reconstruct the proofs as automated theorem proving. We are aiming to implement them “accurately” on Isabelle/ HOL and have done so for many of them. This is the originality of this study.