Unsolvability of the Quintic Formalized in Dependent Type Theory
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub · VU Research Portal · 2021
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.