Proving the Impossibility of Trisecting an Angle and Doubling the Cube

Title:	Proving the Impossibility of Trisecting an Angle and Doubling the Cube
Authors:	Ralph Romanos (ralph /dot/ romanos /at/ student /dot/ ecp /dot/ fr) and Lawrence C. Paulson
Submission date:	2012-08-05
Abstract:	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.
BibTeX:	@article{Impossible_Geometry-AFP, author = {Ralph Romanos and Lawrence C. Paulson}, title = {Proving the Impossibility of Trisecting an Angle and Doubling the Cube}, journal = {Archive of Formal Proofs}, month = aug, year = 2012, note = {\url{http://isa-afp.org/entries/Impossible_Geometry.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry