
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: 
20120805 
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_GeometryAFP,
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{https://isaafp.org/entries/Impossible_Geometry.html},
Formal proof development},
ISSN = {2150914x},
}

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.

