Accesso libero

Pappus’s Hexagon Theorem in Real Projective Plane



Summary. 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”’s_hexagon_theorem


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 Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk 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 Prover9

, the successor of the Otter prover and ott2miz by Josef Urban

See its homepage

[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].

Frequenza di pubblicazione:
4 volte all'anno
Argomenti della rivista:
Computer Sciences, other, Mathematics, General Mathematics