Unsolvability of the Quintic Formalized in Dependent Type Theory
Abstract
In this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois’ Theorem of the equivalence between solvable extensions and extensions
solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.
Origin : Files produced by the author(s)