Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP Article: Ptolemy's Theorem

Email Gateway (Aug 22 2022 at 13:56):

From: Tobias Nipkow <nipkow@in.tum.de>
Ptolemy's Theorem
Lukas Bulwahn

This entry provides an analytic proof to Ptolemy's Theorem using polar form
transformation and trigonometric identities. In this formalization, we use ideas
from John Harrison's HOL Light formalization and the proof sketch on the
Wikipedia entry of Ptolemy's Theorem. This theorem is the 95th theorem of the
Top 100 Theorems list.

https://www.isa-afp.org/entries/Ptolemys_Theorem.shtml

Only 29 theorems to go...
smime.p7s

Last updated: Apr 26 2024 at 16:20 UTC