Abel-Ruffini theorem announced in Coq

Stream: maths

[François Sunatori]

Someone on the Coq discourse has announced this week that they have formalized the Abel-Ruffini theorem:
https://coq.discourse.group/t/a-formal-proof-of-abel-ruffini-theorem-in-coq/1189

Just letting people know if ever it can be of inspiration in Lean.

[Thomas Browning]

Yes, and a few of us are working on it in Lean right now.

[Johan Commelin]

@Cyril Cohen @Assia Mahboubi Congratulations!

[Alex J. Best]

Very cool, @Cyril Cohen writes "NB: all the proofs in this repository are constructive." What does being constructive in this repository give you? I'd imagine that means you can compute in number fields in a verified way, which is already pretty nice, but do you get more out of this theory like an in-principle-computable function that spits out Galois groups of a given nested radical expression, or anything else that a number theorist who likes algorithms might enjoy?

[Kevin Buzzard]

I talked to Cyril about this recently. I think it's just a cultural difference, I don't think they're claiming that they can compute anything in practice, it's just that they will do everything constructively if it's possible because basically they've been brainwashed or however you want to call it -- they just have this convinction that it's important to be constructive whenever you can.

[Patrick Massot]

I would be very surprised if this kind of constructive buy you anything that looks like a computer algebra system use.

[Kevin Buzzard]

Right, but of course if people want to work that way then it's fine. Maybe it makes the code cleaner somehow? I remember when we had a constructive definition of valuation (instead of v(a+b) <= max(v(a),v(b)) we had v(a+b) <= v(a) or v(a+b) <= v(b)) in the perfectoid project and it drove us nuts! So we changed it and refactored. My impression when I was formalising some topology constructively was that it actually made the arguments harder to read. But it's still very clear that there are a lot of people taking constructivism seriously in computer science departments, for good reasons, and it's just somehow a culture leak.

[Cyril Cohen]

@Kevin Buzzard

basically they've been brainwashed or however you want to call it

Seriously?

[Cyril Cohen]

Johan Commelin said:

Cyril Cohen Assia Mahboubi Congratulations!

Thanks @Johan Commelin

[Cyril Cohen]

Alex J. Best said:

Very cool, Cyril Cohen writes "NB: all the proofs in this repository are constructive." What does being constructive in this repository give you? I'd imagine that means you can compute in number fields in a verified way, which is already pretty nice, but do you get more out of this theory like an in-principle-computable function that spits out Galois groups of a given nested radical expression, or anything else that a number theorist who likes algorithms might enjoy?

At this stage it means e.g. that it is decidable whether a polynomial is solvable or not, so it is a theoretical computational result that this algorithm exists and we could in principle run it and it would probably take more than your lifespan to return, without further optimization (although one might argue that there is no difference in practice between non-decidable and terminating in a time that is too long for our workday/carrier/lifespan, still.)

It is also asserting that the result holds in other foundations of mathematics than ZFC: as it is stated the results holds in CIC + a few universes, i.e. Coq with no additional axioms. This means it would hold in the computable fragment of Lean, if there were a translation from Coq to Lean, but also, e.g., in CIC + algebraic universes + axiom of choice (i.e. as in the noncomputable mode of Lean), as well as in CIC + Univalent Foundations.

Somehow, given the library we already have, it does not cost much more to prove this version that the "non computable/classical" one, so we might as well do it.

[Kevin Buzzard]

@Cyril Cohen of course I jest ;-) but it's certainly true that I cannot really see the point, even though you have tried to explain it to me in the past

[Alex J. Best]

@Cyril Cohen Thanks! Personally I do think its quite interesting to know what is in principle computable completely rigorously (of course computing anything nontrivial in most cases requires a different implementation to the mathematically nice ones). CASes like Pari make all sorts of assumptions, like GRH when computing class groups, normally only to speed things up but there are often heuristics about how much precision is needed in various contexts that without studying the source code it is hard to understand exactly what is assumed vs proved (this isn't a criticism of Pari of course its good that it does these things to be fast, just sometimes I'd like to be more sure of my proofs). I spent some time in the past very confused as to what is even computationally provable when Pari says that the (analytic) rank of elliptic curve is some number. I believe it is still an open problem to prove that any elliptic curve has _analytic_ rank $\ge 4$ for instance. I've not thought too much about Galois groups, but given that some of the general algorithms seem to use real or p-adic computation to some precision its a nice side output of the formalization to know there is a verified decision procedure for solvability!