<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. 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 <italic>A, B, C</italic>, and another set of collinear points <italic>a, b, c</italic>, then the intersection points <italic>X, Y, Z</italic> of line pairs <italic>Ab</italic> and <italic>aB, Ac</italic> and <italic>aC, Bc</italic> and <italic>bC</italic> are collinear”<fn id="j_forma-2021-0007_fn_2" symbol="2"><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem">https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem</ext-link></fn>.
More precisely, we prove that the structure <monospace>ProjectiveSpace TOP-REAL3</monospace> [10] (where <monospace>TOP-REAL3</monospace> 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 <monospace>Prover9</monospace><fn id="j_forma-2021-0007_fn_3" symbol="3"><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://www.cs.unm.edu/~mccune/prover9/">https://www.cs.unm.edu/~mccune/prover9/</ext-link></fn>, the successor of the <monospace>Otter</monospace> prover and <monospace>ott2miz</monospace> by Josef Urban<fn id="j_forma-2021-0007_fn_4" symbol="4">See its homepage <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://github.com/JUrban/ott2miz">https://github.com/JUrban/ott2miz</ext-link></fn> [13], [8], [7].
In <monospace>Coq</monospace>, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].
</abstract>

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”https://en.wikipedia.org/wiki/Pappus’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 Prover9https://www.cs.unm.edu/~mccune/prover9/, the successor of the Otter prover and ott2miz by Josef UrbanSee its homepage https://github.com/JUrban/ott2miz [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].

Pappus’s Hexagon Theorem in Real Projective Plane

Formalized Mathematics

{"article-title":"Pappus\u2019s 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,...

Pappus’s Hexagon Theorem in Real Projective Plane

Article Category: Artikel

Data publikacji: 30 gru 2021

Zakres stron: 69 - 76

Przyjęty: 30 cze 2021

DOI: https://doi.org/10.2478/forma-2021-0007

Słowa kluczowe
Pappus’s Hexagon Theorem, real projective plan, Grassmann-Plücker relation, Prover9

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Pappus’s Hexagon Theorem in Real Projective Plane

Article Category: Artikel

Data publikacji: 30 gru 2021

Zakres stron: 69 - 76

Przyjęty: 30 cze 2021

DOI: https://doi.org/10.2478/forma-2021-0007

Słowa kluczowePappus’s Hexagon Theorem, real projective plan, Grassmann-Plücker relation, Prover9

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Słowa kluczowe
Pappus’s Hexagon Theorem, real projective plan, Grassmann-Plücker relation, Prover9