Stream: math-comp users

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


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

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 here.

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.

view this post on Zulip Karl Palmskog (Jan 13 2021 at 17:16):

so is this the first full formalization of Abel-Ruffini? I guess the recent formalization work presented at Lean Together is quite different conceptually? Or how do they compare?

view this post on Zulip Karl Palmskog (Jan 13 2021 at 17:19):

by the way, I think this deserves a CoqLang tweet @Anton Trunov @Emilio Jesús Gallego Arias

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

The work presented at the lean together workshop was a road map towards Abel-Ruffini, they are not there yet.

view this post on Zulip Anton Trunov (Jan 13 2021 at 17:20):

Yep, was typing the tweet this instant :)

view this post on Zulip Karl Palmskog (Jan 13 2021 at 17:22):

Cyril Cohen said:

The work presented at the lean together workshop was a road map towards Abel-Ruffini, they are not there yet.

I suspected as much, but they also aim to prove it in a quite different way, right?

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

It's the same proof, although the tools and fundations are not exactly the same, they should look alike

view this post on Zulip Karl Palmskog (Jan 13 2021 at 17:27):

ah OK, then I might've misunderstood something in the talk.

view this post on Zulip Enrico Tassi (Jan 13 2021 at 17:28):

Can you do something to make 2%:Q%:P look less ugly?

view this post on Zulip Enrico Tassi (Jan 13 2021 at 17:30):

I mean, for the sake of the example, I would not mind locally adding ad hoc notations for numbers

view this post on Zulip Enrico Tassi (Jan 13 2021 at 17:32):

Anyway, chapeau !

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

Ahah, right, I could do that... but I'm done for today

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

Actually I think we should try to make numerals work in the ring scope now...

view this post on Zulip Cyril Cohen (Jan 13 2021 at 23:07):

Enrico Tassi said:

Can you do something to make 2%:Q%:P look less ugly?

I took care of this!

view this post on Zulip Bas Spitters (Jan 14 2021 at 10:22):

Once the lean proof is finished it would be quite an interesting point of comparison.

view this post on Zulip Reynald Affeldt (Jan 27 2021 at 13:25):

“Oh, l’Abel-preuve !”


Last updated: Feb 08 2023 at 04:04 UTC