Document Open Access Logo

Unsolvability of the Quintic Formalized in Dependent Type Theory

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.8.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Sophie Bernard
  • Université Côte d'Azur, Inria, Sophia Antipolis, France
Cyril Cohen
  • Université Côte d'Azur, Inria, Sophia Antipolis, France
Assia Mahboubi
  • Inria, Nantes, France
  • Vrije Universiteit Amsterdam, The Netherlands
Pierre-Yves Strub
  • École Polytechnique, Palaiseau, France

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2021.8

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
  • Theory of computation → Constructive mathematics
Keywords
  • Galois theory
  • Coq
  • Mathematical Components
  • Dependent Type Theory
  • Abel-Ruffini
  • General quintic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Peter Aczel. Galois: a theory development project. manuscript, University of Manchester, 1993. Google Scholar
  2. Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner. Internalizing representation independence with univalence. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434293.
  3. Gilles Barthe. A formal proof of the unsolvability of the symmetric group over a set with five or more elements. URL: https://ftp.cs.ru.nl/CSI/CompMath.Found/sn.ps.Z.
  4. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for Free! In Certified Programs and Proofs, pages 147-162, Melbourne, Australia, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_10.
  5. Cyril Cohen and Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science, 8(1:02):1-40, 2012. URL: https://doi.org/10.2168/LMCS-8(1:02)2012.
  6. Paulo Emílio de Vilhena and Lawrence C. Paulson. Algebraically closed fields in isabelle/hol. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 204-220, Cham, 2020. Springer International Publishing. Google Scholar
  7. Maxime Dénès, Anders Mörtberg, and Vincent Siles. A refinement-based approach to computational algebra in COQ. In Lennart Beringer and Amy Felty, editors, ITP - 3rd International Conference on Interactive Theorem Proving - 2012, volume 7406 of Lecture Notes In Computer Science, pages 83-98, Princeton, United States, August 2012. Springer. URL: https://doi.org/10.1007/978-3-642-32347-8_7.
  8. Evariste Galois. Mémoire sur les conditions de résolubilité des équations par radicaux, volume XI of Journal de mathématiques pures et appliquées. Joseph Liouville, 1846. URL: https://www.bibnum.education.fr/sites/default/files/galois_memoire_sur_la_resolubiblite.pdf.
  9. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging Mathematical Structures. working paper or preprint, 2009. URL: https://hal.inria.fr/inria-00368403.
  10. Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving - ITP 2011, volume 6898 of Lecture Notes in Computer Science, pages 103-118, Berg en Dal, Netherlands, 2011. Radboud University of Nijmegen, Springer. URL: https://doi.org/10.1007/978-3-642-22863-6_10.
  11. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd Order Theorem. In Sandrine Blazy, Christine Paulin, and David Pichardie, editors, ITP 2013, 4th Conference on Interactive Theorem Proving, volume 7998 of LNCS, pages 163-179, Rennes, France, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39634-2_14.
  12. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. SIGPLAN Not., 46(9):163–175, 2011. URL: https://doi.org/10.1145/2034574.2034798.
  13. Michael Hedberg. A coherence theorem for Martin-Löf’s Type Theory. J. Funct. Program., 8(4):413-436, 1998. URL: https://doi.org/10.1017/S0956796898003153.
  14. Abel Niels Henrik. Œuvres complètes de Niels Henrik Abel, mathématicien, nouvelle édition publiée aux frais de l'État norvégien par L. Sylow et S. Lie. Imprimerie de Grøndahl & søn, 1881. URL: https://www.abelprize.no/c54178/artikkel/vis.html?tid=54181.
  15. Serge Lang. Algebra. Graduate Texts in Mathematics. Springer New York, 2005. Google Scholar
  16. Assia Mahboubi. The rooster and the butterflies. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings, volume 7961 of Lecture Notes in Computer Science, pages 1-18. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39320-4_1.
  17. Assia Mahboubi and Enrico Tassi. Canonical structures for the working coq user. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 19-34, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  18. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  19. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  20. R. Mines, F. Richman, and W. Ruitenburg. A Course in Constructive Algebra. Universitext. Springer New York, 1987. Google Scholar
  21. P. Ruffini. Teoria generale delle equazioni: in cui si dimostra impossibile la soluzione algebraica delle equazioni generali di grad superiore al quarto. Number pt. 1 in Nineteenth Century Collections Online (NCCO): Science, Technology, and Medicine: 1780-1925. Nella stamperia di S. Tommaso d'Aquino, 1799. Google Scholar
  22. Amokrane Saibi. Typing algorithm in type theory with inheritance. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 292-301, 1997. Google Scholar
  23. Christoph Schwarzweller. On roots of polynomials over F[X]/(p). Formaliz. Math., 27(2):93-100, 2019. URL: https://doi.org/10.2478/forma-2019-0010.
  24. Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. Equivalences for free: univalent parametricity for effective transport. Proc. ACM Program. Lang., 2(ICFP):92:1-92:29, 2018. URL: https://doi.org/10.1145/3236787.
  25. The Mathematical Components Team. The Mathematical Components library. https://github.com/math-comp/math-comp, 2007.
  26. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
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 About DROPS Imprint Privacy Contact