[isabelle] New in the AFP: Intersecting Chords Theorem



We now have a small but elegant entry from Lukas Bulwahn:

> This entry provides a geometric proof of the intersecting chords theorem. The theorem states that when two chords intersect each other inside a circle, the products of their segments are equal. After a short review of existing proofs in the literature, I decided to use a proof approach that employs reasoning about lengths of line segments, the orthogonality of two lines and the Pythagoras Law. Hence, one can understand the formalized proof easily with the knowledge of a few general geometric facts that are commonly taught in high-school. This theorem is the 55th theorem of the Top 100 Theorems list.


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

Many thanks, and keep them coming! Incidentally, we are also getting entries to the Development branch of the AFP. These can take advantage of the latest development version of Isabelle but unfortunately will not become visible on the AFP website until after the next release. That is expected by the end of 2016.

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.