Stream: Coq users

Topic: A formal proof of Abel-Ruffini Theorem in Coq


view this post on Zulip Cyril Cohen (Jan 13 2021 at 17:14):

I am happy to announce that we -- Sophie Bernard, Cyril Cohen, Assia Mahboubi and Pierre-Yves Strub -- were able to formalize in Coq a proof of Abel-Ruffini Theorem, which states that there are polynomials of degree 5 that are not solvable by radicals, e.g. X54X+2X^5 - 4X + 2.

Lemma example_not_solvable_by_radicals :
  ~ solvable_by_radical_poly ('X^5 - 4 *: 'X + 2).

This is a consequence of Abel-Galois theorem (also formalized) which states the equivalence between being solvable by radicals and having a solvable Galois group.

The proofs are accessible in the repository https://github.com/math-comp/Abel and will soon be released as the opam package coq-mathcomp-abel.1.0.0 and as a nix package. This development uses and extends non trivially the Mathematical Components library especially the Galois Theory part.
NB: all the proofs in this repository are constructive.

Cyril Cohen, for the contributors of https://github.com/math-comp/Abel

Cross posted to #Coq users and #math-comp users please follow-up on #math-comp users

A proof of Abel-Ruffini theorem. Contribute to math-comp/Abel development by creating an account on GitHub.
Mathematical Components. Contribute to math-comp/math-comp development by creating an account on GitHub.

Last updated: Jan 28 2023 at 06:30 UTC