The version of the project in which it was submitted is here.
The Bachelor's thesis addresses the formalisation of ancient construction problems, with a particular focus on the "Impossibility of Trisecting the Angle and Doubling the Cube". This is the eighth theorem published by Freek Wiedijk in the '100 Theorems' compendium, which serves to allow for a comparison of different theorem provers. For this, the theorem prover Lean is utilised. As a result, this paper is devoted to the problems and solutions that arise when formalising ancient construction problems and proves the impossibility of doing so using Galois' theory.
Die Bachelorarbeit befasst sich mit der Formalisierung antiker Konstruktionsprobleme, wobei der Schwerpunkt auf der „Unmöglichkeit der Dreiteilung des Winkels und der Verdoppelung des Würfels“ liegt. Dies ist das achte Theorem, das Freek Wiedijk in dem im Rahmen von „100 Theorems“ veröffentlichten Kompendium veröffentlicht hat, das dazu dient, einen Vergleich verschiedener Theorembeweiser zu ermöglichen. Hierfür wird der Theorembeweiser Lean verwendet. Die vorliegende Arbeit widmet sich daher den Problemen und Lösungen, die bei der Formalisierung alter Konstruktionsprobleme auftreten, und beweist die Unmöglichkeit, dies mit der Galois-Theorie zu tun.