Dear Coq community,

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. X^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 GitHub - math-comp/Abel: A proof of Abel-Ruffini theorem. 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.

Happy new year and best wishes,

–

Cyril Cohen, for the contributors of GitHub - math-comp/Abel: A proof of Abel-Ruffini theorem.