1 Search Results for "Bernard, Sophie"

Document
DOI: 10.4230/LIPIcs.ITP.2021.8
Unsolvability of the Quintic Formalized in Dependent Type Theory

Authors: Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.
Cite as

Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8,
  author =	{Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves},
  title =	{{Unsolvability of the Quintic Formalized in Dependent Type Theory}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8},
  URN =		{urn:nbn:de:0030-drops-139038},
  doi =		{10.4230/LIPIcs.ITP.2021.8},
  annote =	{Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic}
}
  • Refine by Author
  • 1 Bernard, Sophie
  • 1 Cohen, Cyril
  • 1 Mahboubi, Assia
  • 1 Strub, Pierre-Yves

  • Refine by Classification
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Abel-Ruffini
  • 1 Coq
  • 1 Dependent Type Theory
  • 1 Galois theory
  • 1 General quintic
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact