Zulip Chat Archive

Stream: maths

Topic: Abel-Ruffini theorem announced in Coq


view this post on Zulip François Sunatori (Jan 22 2021 at 04:42):

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.

view this post on Zulip Thomas Browning (Jan 22 2021 at 04:43):

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

view this post on Zulip Johan Commelin (Jan 22 2021 at 05:06):

@Cyril Cohen @Assia Mahboubi Congratulations!

view this post on Zulip Alex J. Best (Jan 22 2021 at 05:23):

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?

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 08:26):

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.

view this post on Zulip Patrick Massot (Jan 22 2021 at 08:31):

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

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 08:37):

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.

view this post on Zulip Cyril Cohen (Jan 22 2021 at 16:37):

@Kevin Buzzard

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

Seriously?

view this post on Zulip Cyril Cohen (Jan 22 2021 at 16:41):

Johan Commelin said:

Cyril Cohen Assia Mahboubi Congratulations!

Thanks @Johan Commelin

view this post on Zulip Cyril Cohen (Jan 22 2021 at 16:53):

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.

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 18:55):

@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

view this post on Zulip Alex J. Best (Jan 22 2021 at 19:35):

@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 4\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!


Last updated: May 10 2021 at 06:13 UTC