HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Sunday, May 2, 2021 - 1:44:47 AM
Last modification on : Wednesday, April 27, 2022 - 3:47:58 AM


Files produced by the author(s)


  • HAL Id : hal-03136002, version 4


Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France. ⟨hal-03136002v4⟩



Record views


Files downloads