Email Gateway (Aug 19 2022 at 08:32): Email Gateway (Aug 19 2022 at 08:32):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC