Email Gateway (Aug 23 2026 at 15:04): Email Gateway (Aug 23 2026 at 15:04):From: Tobias Nipkow <nipkow@in.tum.de>
Miquel's Theorem in Isabelle/HOL
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
We formalize Miquel's theorem, also known as the pivot theorem, in Isabelle/HOL.
Let be a triangle in the Euclidean plane and let ... be points on the side lines
... respectively. Then the circumcircles of the three triangles ... pass through
a common point, the Miquel point of the configuration.
The development uses complex coordinates.
https://isa-afp.org/entries/Miquel.html
Enjoy!
Last updated: Sep 02 2026 at 16:10 UTC