Pappus’s Hexagon Theorem in Real Projective Plane

Abstract

In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points A, B, C, and another set of collinear points a, b, c, then the intersection points X, Y, Z of line pairs Ab and aB, Ac and aC, Bc and bC are collinear”2. More precisely, we prove that the structure ProjectiveSpace TOP-REAL3 [10] (where TOP-REAL3 is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leonczuk and Krzysztof Prazmowski. Eugeniusz Kusak andWojciech Leonczuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” [12]. Secondly, Pascal’s theorem [4] is used. In both cases, to prove some lemmas, we use Prover93, the successor of the Otter prover and ott2miz by Josef Urban4 [13], [8], [7]. In Coq, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].