Miquel's Theorem in Isabelle/HOL

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

August 11, 2026

Abstract

We formalize Miquel's theorem, also known as the pivot theorem, in Isabelle/HOL. Let \(ABC\) be a triangle in the Euclidean plane and let \(P\), \(Q\), \(R\) be points on the side lines \(BC\), \(CA\), \(AB\) respectively. Then the circumcircles of the three triangles \(AQR\), \(BRP\), \(CPQ\) pass through a common point \(M\), the Miquel point of the configuration.

The development uses complex coordinates.

License

BSD License

Note

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

Topics

Session Miquel

Depends on

Cite

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