@ARTICLE{PAPPUS,
    TITLE = {Pappus's Hexagon Theorem in Real Projective Plane},
    AUTHOR = {Coghetto, Roland},
    ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
    DAY = {30},
    MONTH = {June},
    YEAR = {2021},
    SUMMARY = {In this article, we proof 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"\footnote{WIKIPEDIA, https://en.wikipedia.org/wiki/Pappus%27s_hexagon_theorem}).\par
    More precisely, we prove that the structure  
    \verb?ProjectiveSpace TOP-REAL 3? \cite{ANPROJ_1.ABS} (where \verb?TOP-REAL 3? 
    is a metric space defined in \cite{EUCLID.ABS}) 
    satisfies the Pappus's axiom defined in \cite{ANPROJ_2.ABS} 
    by Wojciech Leo{\'n}czuk and Krzysztof Pra{\.z}mowski. 
    Eugeniusz Kusak and Wojciech Leo\'nczuk formalized the Hessenberg theorem early 
    in the MML \cite{HESSENBE.ABS}. With this result, the real projective plane 
    is Desarguesian.\par
    For proving the Pappus theorem, two different proofs are given.\par
    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"\cite{Richter-Gebert2011}.\par
    Secondly, Pascal's theorem \cite{PASCAL.ABS} is used.\par
    In both cases, to prove somme lemmas, we use 
    \verb?PROVER9?\footenote{https://www.cs.unm.edu/~mccune/prover9/}, 
    the successor of the Otter prover and \verb?OTT2MIZ? by Joseph Urban, 
    \footnote{See its homepage https://github.com/JUrban/ott2miz}
    \cite{rudnicki2011escape,grabowski2006solving,grabowski2015mechanizing}. \par
    In Coq, the Pappus's theorem is proved as the application of 
    Grassmann-Cayley algebra \cite{fuchs2010formalization} and more recently 
    in Tarski's geometry \cite{braun2015synthetic}.},
    MSC2010 = {51N15,03B35,68V20},
    KEYWORDS = {Pappus Hexagon Theorem, real projective plan, Grassman-Pl{�}ucker relation, prover9}
}

@inproceedings{fuchs2010formalization,
  title={A formalization of grassmann-cayley algebra in COQ and its application to theorem proving in projective geometry},
  author={Fuchs, Laurent and Th{\'e}ry, Laurent},
  booktitle={International Workshop on Automated Deduction in Geometry},
  pages={51--67},
  year={2010},
  organization={Springer}
}

@article{braun2015synthetic,
  title={A synthetic proof of Pappus’ theorem in Tarski’s geometry},
  author={Braun, Gabriel and Narboux, Julien},
  journal={Journal of Automated Reasoning},
  pages={1--22},
  publisher={Springer}
}

@article{grabowski2006solving,
  title={Solving Two Problems in General Topology Via Types},
  author={Grabowski, Adam},
  journal={Types for Proofs and Programs},
  pages={138--153},
  year={2006},
  publisher={Springer}
}
@article{grabowski2015mechanizing,
  title={Mechanizing complemented lattices within Mizar type system},
  author={Grabowski, Adam},
  journal={Journal of Automated Reasoning},
  volume={55},
  number={3},
  pages={211--221},
  year={2015},
  publisher={Springer}
}
@inproceedings{rudnicki2011escape,
  title={Escape to ATP for Mizar},
  author={Rudnicki, Piotr and Urban, Josef},
  booktitle={First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011},
  year={2011}
}

@Inbook{Richter-Gebert2011,
author="Richter-Gebert, J{\"u}rgen",
title="Pappos's Theorem: Nine Proofs and Three Variations",
bookTitle="Perspectives on Projective Geometry: A Guided Tour Through Real and Complex Geometry",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="3--31",
isbn="978-3-642-17286-1",
doi="10.1007/978-3-642-17286-1_1",
url="http://dx.doi.org/10.1007/978-3-642-17286-1_1"
}

@article{alama2012escape,
  title={Escape to Mizar for ATPs},
  author={Alama, Jesse},
  journal={arXiv preprint arXiv:1204.6615},
  year={2012}
}

