@inproceedings{86a7d1b259244422bbd26d08ac8ae535,
title = "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.",
keywords = "Abel-Ruffini, Coq, Dependent Type Theory, Galois theory, General quintic, Mathematical Components",
author = "Sophie Bernard and Cyril Cohen and Assia Mahboubi and Strub, \{Pierre Yves\}",
note = "Publisher Copyright: {\textcopyright} Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub.; 12th International Conference on Interactive Theorem Proving, ITP 2021 ; Conference date: 29-06-2021 Through 01-07-2021",
year = "2021",
month = jun,
day = "1",
doi = "10.4230/LIPIcs.ITP.2021.8",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Liron Cohen and Cezary Kaliszyk",
booktitle = "12th International Conference on Interactive Theorem Proving, ITP 2021",
}