Ssreflect Users Discussion List

[Cyril Cohen <>]

Dear Coq-club and ssreflect mailing list,

I am happy to announce that we -- Sophie Bernard, Cyril Cohen, Assia 
Mahoubi 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. $X^5 - 4X + 2$.
```coq
Lemma example_not_solvable_by_radicals :
  ~ solvable_by_radical_poly ('X^5 - 4%:R *: 'X + 2%:Q%:P).
```
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](https://github.com/math-comp/math-comp) especially the Galois 
Theory part.
NB: all the proofs in this repository are constructive.

Happy new year and best wishes,
--
Cyril Cohen, for the contributors of https://github.com/math-comp/Abel