Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Napoleon's theorem

view this post on Zulip Email Gateway (Sep 18 2026 at 14:11):

From: Lawrence Paulson <lp15@cam.ac.uk>

I'm happy to announce another contribution by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz.

Napoleon's Theorem

Napoleon's theorem states that, for a non-degenerate triangle, the centres of the equilateral triangles constructed externally on its three sides form an equilateral triangle. We formalize this construction and conclusion using complex coordinates, including the exterior-side condition and both orientations of the 60-degree rotation.

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

Larry

Last updated: Oct 08 2026 at 21:07 UTC