{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T01:07:39Z","timestamp":1783904859555,"version":"3.55.0"},"reference-count":13,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T00:00:00Z","timestamp":1625097600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,7,1]]},"abstract":"\n Summary<\/jats:bold>\n . In this article we prove, using Mizar [2], [1], the Pappus\u2019s hexagon theorem in the real projective plane: \u201cGiven one set of collinear points\n A, B, C<\/jats:italic>\n , and another set of collinear points\n a, b, c<\/jats:italic>\n , then the intersection points\n X, Y, Z<\/jats:italic>\n of line pairs\n Ab<\/jats:italic>\n and\n aB, Ac<\/jats:italic>\n and\n aC, Bc<\/jats:italic>\n and\n bC<\/jats:italic>\n are collinear\u201d\n \n \n https:\/\/en.wikipedia.org\/wiki\/Pappus\u2019s_hexagon_theorem<\/jats:ext-link>\n <\/jats:p>\n <\/jats:fn>\n .\n <\/jats:p>\n \n More precisely, we prove that the structure\n ProjectiveSpace TOP-REAL3<\/jats:monospace>\n [10] (where\n TOP-REAL3<\/jats:monospace>\n is a metric space defined in [5]) satisfies the Pappus\u2019s axiom defined in [11] by Wojciech Leo\u0144czuk and Krzysztof Pra\u017cmowski. Eugeniusz Kusak and Wojciech Leo\u0144czuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus\u2019s theorem, two different proofs are given. First, we use the techniques developed in the section \u201cProjective Proofs of Pappus\u2019s Theorem\u201d in the chapter \u201cPappos\u2019s Theorem: Nine proofs and three variations\u201d [12]. Secondly, Pascal\u2019s theorem [4] is used.\n <\/jats:p>\n \n In both cases, to prove some lemmas, we use\n Prover9<\/jats:monospace>\n \n \n https:\/\/www.cs.unm.edu\/~mccune\/prover9\/<\/jats:ext-link>\n <\/jats:p>\n <\/jats:fn>\n , the successor of the\n Otter<\/jats:monospace>\n prover and\n ott2miz<\/jats:monospace>\n by Josef Urban\n \n \n See its homepage\n https:\/\/github.com\/JUrban\/ott2miz<\/jats:ext-link>\n <\/jats:p>\n <\/jats:fn>\n [13], [8], [7].\n <\/jats:p>\n \n In\n Coq<\/jats:monospace>\n , the Pappus\u2019s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski\u2019s geometry [3].\n <\/jats:p>","DOI":"10.2478\/forma-2021-0007","type":"journal-article","created":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T01:55:57Z","timestamp":1641434157000},"page":"69-76","source":"Crossref","is-referenced-by-count":0,"title":["Pappus\u2019s Hexagon Theorem in Real Projective Plane"],"prefix":"10.2478","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4901-0766","authenticated-orcid":false,"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"cafr-MSA2P asbl Rue de la Brasserie 5 La Louvi\u00e8re , Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2021,12,30]]},"reference":[{"key":"2026071214195361377_j_forma-2021-0007_ref_1","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071214195361377_j_forma-2021-0007_ref_2","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.10.1007\/s10817-017-9440-6604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071214195361377_j_forma-2021-0007_ref_3","doi-asserted-by":"crossref","unstructured":"Gabriel Braun and Julien Narboux. A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry. Journal of Automated Reasoning, 58(2):23, 2017. doi:10.1007\/s10817-016-9374-4.10.1007\/s10817-016-9374-4","DOI":"10.1007\/s10817-016-9374-4"},{"key":"2026071214195361377_j_forma-2021-0007_ref_4","doi-asserted-by":"crossref","unstructured":"Roland Coghetto. Pascal\u2019s theorem in real projective plane. Formalized Mathematics, 25(2):107\u2013119, 2017. doi:10.1515\/forma-2017-0011.10.1515\/forma-2017-0011","DOI":"10.1515\/forma-2017-0011"},{"key":"2026071214195361377_j_forma-2021-0007_ref_5","unstructured":"Agata Darmochwa\u0142. The Euclidean space. Formalized Mathematics, 2(4):599\u2013603, 1991."},{"key":"2026071214195361377_j_forma-2021-0007_ref_6","doi-asserted-by":"crossref","unstructured":"Laurent Fuchs and Laurent Thery. A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry. In Automated Deduction in Geometry, pages 51\u201367. Springer, 2010.10.1007\/978-3-642-25070-5_3","DOI":"10.1007\/978-3-642-25070-5_3"},{"key":"2026071214195361377_j_forma-2021-0007_ref_7","doi-asserted-by":"crossref","unstructured":"Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211\u2013221, 2015. doi:10.1007\/s10817-015-9333-5.10.1007\/s10817-015-9333-5","DOI":"10.1007\/s10817-015-9333-5"},{"key":"2026071214195361377_j_forma-2021-0007_ref_8","unstructured":"Adam Grabowski. Solving two problems in general topology via types. In Types for Proofs and Programs, International Workshop, TYPES 2004, Jouyen-Josas, France, December 15-18, 2004, Revised Selected Papers, pages 138\u2013153, 2004. doi:10.1007\/11617990_9. http:\/\/dblp.uni-trier.de\/rec\/bib\/conf\/types\/Grabowski04.10.1007\/11617990_9"},{"key":"2026071214195361377_j_forma-2021-0007_ref_9","unstructured":"Eugeniusz Kusak and Wojciech Leo\u0144czuk. Hessenberg theorem. Formalized Mathematics, 2(2):217\u2013219, 1991."},{"key":"2026071214195361377_j_forma-2021-0007_ref_10","unstructured":"Wojciech Leo\u0144czuk and Krzysztof Pra\u017cmowski. A construction of analytical projective space. Formalized Mathematics, 1(4):761\u2013766, 1990."},{"key":"2026071214195361377_j_forma-2021-0007_ref_11","unstructured":"Wojciech Leo\u0144czuk and Krzysztof Pra\u017cmowski. Projective spaces \u2013 part I. Formalized Mathematics, 1(4):767\u2013776, 1990."},{"key":"2026071214195361377_j_forma-2021-0007_ref_12","unstructured":"J\u00fcrgen Richter-Gebert. Pappos\u2019s Theorem: Nine Proofs and Three Variations, pages 3\u201331. Springer Berlin Heidelberg, 2011. ISBN 978-3-642-17286-1. doi:10.1007\/978-3-642-17286-1_1.10.1007\/978-3-642-17286-1_1"},{"key":"2026071214195361377_j_forma-2021-0007_ref_13","unstructured":"Piotr Rudnicki and Josef Urban. Escape to ATP for Mizar. In First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2021-0007","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:22:13Z","timestamp":1783902133000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2021-0007"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,1]]},"references-count":13,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2021,12,30]]},"published-print":{"date-parts":[[2021,7,1]]}},"alternative-id":["10.2478\/forma-2021-0007"],"URL":"https:\/\/doi.org\/10.2478\/forma-2021-0007","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,1]]}}}