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

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Proving the Impossibility of Trisecting an Angle and Doubling the Cube}
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Mon, 06 Aug 2012 22:30:26 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

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.*