[isabelle] New AFP entry: Proving the Impossibility of Trisecting an Angle and Doubling the Cube}



Proving the Impossibility of Trisecting an Angle and Doubling the Cube
Ralph Romanos and Lawrence Paulson

Squaring the circle, doubling the cube and trisecting an angle, using a compass
and straightedge alone, are classic unsolved problems first posed by the ancient
Greeks. All three problems were proved to be impossible in the 19th century. The
following document presents the proof of the impossibility of solving the latter
two problems using Isabelle/HOL, following a proof by Carrega. The proof uses
elementary methods: no Galois theory or field
extensions. The set of points constructible using a compass and straightedge is
defined inductively. Radical expressions, which involve only square roots and
arithmetic of rational numbers, are defined, and we find that all constructive
points have radical coordinates. Finally, doubling the cube and trisecting
certain angles requires solving certain cubic equations that can be proved to
have no rational roots. The Isabelle proofs require a great many detailed
calculations.

http://afp.sourceforge.net/entries/Impossible_Geometry.shtml

If you would like to hear Larry talk about it, do come to the Isabelle workshop
coming weekend: http://www21.in.tum.de/~nipkow/Isabelle2012/

Enjoy!
Tobias





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