formalize proof of Catalan's conjecture or cyclotomic IMC?

Stream: maths

[Jz Pan]

I'm curious to ask that how far can we formalize the proof of Catalan's conjecture, or cyclotomic Iwasawa Main Conjecture in Lean? These two seems far more easier than formalizing FLT. The first can be found on Schoof's Universitext book "Catalan's conjecture", and the second can be found on the appendix of Washington's GTM cyclotomic field.

[Kevin Buzzard]

I agree that both of these things are doable and much easier than formalizing FLT (but they might not be easier than formalizing an R=T theorem and reducing FLT to theorems from the 1980s, which is what my job is right now). The original Catalan proof doesn't need anything like strong effective Baker bounds, and whilst the Mazur-Wiles IMC proof is probably a tall order, the proof using cyclotomic units is surely feasible. Both projects probably need a leader though, and a leader probably has to be someone who's doing some kind of approximation to "working full time on the project".

[Jz Pan]

Kevin Buzzard said:

Both projects probably need a leader though, and a leader probably has to be someone who's doing some kind of approximation to "working full time on the project".

I agree. My feeling is that merely formalizing a single new concept and corresponding results in standard textbook is already time consuming.

For the IMC, I prefer cyclotomic unit proof with Euler system argument. But for Mazur-Wiles' proof, I think we already have Eisenstein series in Lean, so maybe it's not necessary infeasible?

[Kevin Buzzard]

It's much harder than the Euler system proof because it needs very delicate results about the geometry of modular curves. The Mazur-Wiles paper is around 150 pages isn't it? The Euler system argument is far shorter.

[Filippo A. E. Nuccio]

At any rate, even for the cyclotomic unit proof of IMC we need the full strength of global class field theory.

[Jz Pan]

FYI, currently Mihăilescu is giving a short course at BIMSA https://bimsa.net/activity/CyclotomicFieldsIwasawaTheory/ with Zoom link. Videos available. It's claimed that there will be a simpler proof of Catalan's conjecture.