Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: 2 * Steiner

Email Gateway (Oct 06 2026 at 19:17):

From: Tobias Nipkow <nipkow@in.tum.de>

1. The Steiner Deltoid as the Tangent Envelope of Wallace--Simson Lines in
   Isabelle/HOL
   Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz

We formalize the classical Steiner deltoid construction in Isabelle/HOL using
only the published Archive of Formal Proofs entry for the Wallace--Simson line.
In unit-circumcircle coordinates, the deltoid has an explicit complex
parametrisation. We prove its derivative formula, characterize the stationary
parameters by , and certify them as ordinary cusps using the second and third
derivatives. We then prove an equality of sets between the appropriate
Wallace--Simson line and the tangent line, for every parameter, including the
cusp cases. The development uses complex coordinates and handles a vertex
parameter by cycling to the alternate pair of feet.

https://isa-afp.org/entries/Steiner_Deltoid.html

2. Steiner's Line Theorem in Isabelle/HOL
   Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz

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.

https://isa-afp.org/entries/Steiner_Line_Theorem.html

Enjoy!

smime.p7s

Last updated: Oct 08 2026 at 21:07 UTC