Steiner's Line Theorem in Isabelle/HOL

Arthur Freitas Ramos 📧, David Barros Hulak 📧 and Ruy Jose Guerra Barretto de Queiroz 📧

October 6, 2026

Abstract

We formalize Steiner's line theorem in Isabelle/HOL. For a nondegenerate triangle and a point on its circumcircle, the reflections of that point in the three sidelines are collinear, and the resulting line passes through the orthocenter. The development uses complex coordinates and imports the published Wallace–Simson line entry for its perpendicular-foot and collinearity infrastructure.

License

BSD License

Note

AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.

Topics

Related publications

  • Coxeter, H., & Greitzer, S. (1967). Geometry Revisited. Anneli Lax New Mathematical Library. https://doi.org/10.5948/upo9780883859346

Session Steiner_Line_Theorem

Depends on

Cite

× 
@article{Steiner_Line_Theorem-AFP,
  author  = {Arthur Freitas Ramos and David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz},
  title   = {Steiner's Line Theorem in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Steiner_Line_Theorem.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download