The Coq mailing list

[Cyril Cohen <cyril.cohen AT inria.fr>]

Even though everyone on the mailinglists may correct the typo 
themselves, I believe this deserves an erratum: Assia *Mahboubi*
--
Cyril

On 13/01/2021 18:10, Cyril Cohen wrote:
> 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,