Email Gateway (Aug 05 2026 at 08:53): Email Gateway (Aug 05 2026 at 08:53):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: The Wallace--Simson Line Theorem in Isabelle/HOL
The Wallace--Simson Line Theorem in Isabelle/HOL
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
We formalize the Wallace--Simson line theorem in Isabelle/HOL. Let ABC be a
nondegenerate triangle and let M be a point on its circumcircle. Dropping the
perpendiculars from M to the three side lines gives feet P, Q, R; the theorem
asserts that P,Q,R are collinear. The line through them is the Simson line, also
called the Wallace line after William Wallace, whose published work on
geometrical porisms is the standard early source for this result. We also prove
the converse: if the three feet are collinear, then lies on the circumcircle of
ABC. The development uses complex coordinates.
https://isa-afp.org/entries/Simson.html
Enjoy!
Last updated: Aug 12 2026 at 20:47 UTC