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

https://hal.inria.fr/hal-03136002
Contributor : Cyril Cohen <>
Submitted on : Wednesday, April 21, 2021 - 11:55:11 AM
Last modification on : Tuesday, May 4, 2021 - 3:35:07 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03136002, version 3

Citation

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-03136002v3⟩

Share

Metrics

Record views

37

Files downloads

114