Mason-Stothers theorem and Polynomial FLT

Stream: mathlib4

[Jineon Baek]

Hello. A couple months ago, with suggestion from @Kevin Buzzard me and @Seewoo Lee formalized Mason-Stothers theorem in Lean 3 here.

A consequence of this theorem is a version of FLT on polynomials: if K is a characteristic zero field, then for any polynomials a, b, c in K[X] and n >= 3, the equation a^n + b^n = c^n implies that a, b, c are scalar multiples of a common polynomial.

Now that I see the statement of FLT in mathlib4, I am wondering if porting the Mason-Stothers theorem to mathlib4 is suitable. The proof of both Mason-Stothers and polynomial FLT are elementary, and a full Lean 3 formalization exists, so it shouldn't take that long if one decides to actually port it.

So the questions are:

• Will it be good for mathlib4 to have this theorem? Have a look at the Lean 3 project readme to get a feeling of what the theorem is.
• If so, how can we (@Jineon Baek and @Seewoo Lee) start? Should we start by using mathport to convert our Lean 3 project?

[Yury G. Kudryashov]

• Yes, it will be good for Mathlib to have this theorem. I don't have to be an expert in this area to answer that question.
• I'm not an expert in this area, so I can't comment about your approach to formalizing this theorem (e.g., which proof to use etc).
• Yes, mathport should give you a good first approximation to Lean 4 forward-port.

[Yaël Dillies]

Yep this is definitely a good candidate for inclusion in mathlib

[Kevin Buzzard]

Is docs#FermatLastTheoremWith sufficiently general for it to apply to your work? That would be a nice bonus! Or are there problems with units or something?

[Jineon Baek]

Thanks for the input everyone.

@Kevin Buzzard Unfortunately our polynomial FLT does not match with FermatLastTheoremWith as-is. FermatLastTheoremWith states that every nonzero a, b, c cannot satisfy the FLT equation, but for polynomial with arbitrary field K one may have nonzero scalar (unit) solutions a = b = 1 and c = 2^{1/n}. And also note that their common multiples are also solutions to FLT (the non-coprime solutions).

The question is whether we should a suitable statement of FLT for general semiring that can accommodate this, or should we treat polynomial FLT as a separate theorem.

• A common statement that works is: if a, b, c satisfies a^n+b^n=c^n then a, b, c are common multiples of units. This loses the simplicity of the original FLT on N.
• Another way is to just factor out the equation a^n+b^n=c^n and draw different conclusions for different semirings
• Here is a discussion on FLT for integer matrices.

[Kevin Buzzard]

Yes it's very strange isn't it -- "Fermat's Last Theorem for K" seems to say "if n>=3 then the only solutions to x^n+y^n=z^n in K are the obvious ones" but it's perhaps not possible to formalise what "obvious" means.

[Eric Rodriguez]

Is it enough to posit solutions with no divisibility relations?

[Jineon Baek]

I think you mean that none of a, b, c should divide any other, right? Or is it that it suffices to think of only solutions of that kind?

[Yaël Dillies]

One of the motivations for FermatLastTheoremWith was polynomial FLT, so I'm very much in favour of changing the definition so that it fits it!

[Jineon Baek]

We (@Jineon Baek and @Seewoo Lee) will work on porting our Lean 3 project to Lean 4 for mathlib integration, hopefully in next month or two.

Indeed, separately I think it is worth thinking about what is the right generalization of FLT for general ring. The following text gives a good overview of FLT generalized to number fields. See the counterexamples on Section 3.2, and Theorems 12 and 13. I wonder what characteristics of FLT does make it really work.
https://revistas.rcaap.pt/boletimspm/article/view/21033/15548

Here is an attempt: For any commutative ring A, units u v and w in A, and variables x, y, z in A, the solutions of equation u*x^n + v*y^n + w*z^n = 0 satisfy one of the followings: xyz=0, or there is a common divisor d of x, y, z such that x/d, y/d, z/d are units of A.
I'm not 100% satisfied with this, but this works for at least Z and k[X] where char k = 0.

[Jineon Baek]

We just finished porting our Lean 3 formalization of polynomial FLT to Lean 4:

https://github.com/seewoo5/lean-poly-abc

Now we are ready to include this to mathlib4. The current code is not up to standards of mathlib4 as of now. Any pointers on how to start the process of shpping this to mathlib4?

[Ruben Van de Velde]

Pick a small part and make a pull request

[Kim Morrison]

You should update the README which still says Lean 3!

[Kim Morrison]

Working file at a time is often good. So start with something like https://github.com/seewoo5/lean-poly-abc/blob/main/LeanPolyABC/Lib/RationalFunc.lean, which has no other imports from your project, and start working out which Mathlib files those results should be distributed into. Even just processing that file should be at least one PR.

[Jineon Baek]

Kevin Buzzard said:

Yes it's very strange isn't it -- "Fermat's Last Theorem for K" seems to say "if n>=3 then the only solutions to x^n+y^n=z^n in K are the obvious ones" but it's perhaps not possible to formalise what "obvious" means.

We need to decide if we want to change the statement of docs#FermatLastTheoremWith to incorporate the polynomial FLT or not. I opt to say no (and thus make the polynomial FLT a separate theorem).

For the usual (semi)rings R = N, Z, Q, the following statement suffices and is the current definition of docs#FermatLastTheoremWith.

Statement 1: If n >= 3, then any solution of a^n+b^n=c^n in ring R should satisfy abc=0.

For the polynomial ring R=k[X], its FLT variant is not Statement 1. It should be this instead.

Statement 2: If n >= 3, then any solution of a^n+b^n=c^n in ring R is a common multiple (a, b, c) = (u*d, v*d, w*d) of units or zeroes u, v, w of R.

Now Statement 1 works for R = N, Z, Q but not k[X]. Statement 2 works for R = N, Z, k[X] but not Q (which is stated in Mathlib). The second statement is also lengthier to state and more distant from the original FLT statement. This is why I opt to not change docs#FermatLastTheoremWith and state the polynomial FLT separately.

[Jineon Baek]

In retrospective, we might instead take this approach.

Instead of generalizing FLT to only ring R, we can generalize the statement to R and its subset S of 'trivial' elements, closed under multiplication.

Statement 3: If n >= 3, then any solution of a^n+b^n=c^n in ring R is a common multiple of triples in S.

This captures the idea that the only solutions are 'obvious' ones, by making explicit of what 'obvious' means. Now this works for (N, {0, 1}), (Z, {-1, 0, 1}), (Q, {-1, 0, 1}) and (k[X], k) where they are the pairs (R, S). I'll leave the rest for discussion as this is more of an 'aesthetic' decision.

[Scott Carnahan]

For Statement 1, do you mean abc = 0 to cover cases like a = 0, b = c nonzero?

[Yaël Dillies]

Oh that's a shame. I wrote FermatLastTheoremWith with the explicit goal of including Mason-Stothers

[Yaël Dillies]

Sorry, I missed your second message. Not a shame anymore :)

[Jineon Baek]

Scott Carnahan said:

For Statement 1, do you mean abc = 0 to cover cases like a = 0, b = c nonzero?

Thanks for the catch! It should be abc=0 instead of a=b=c=0.

[Jineon Baek]

Made a PR suggesting a possible generalized statement.

https://github.com/leanprover-community/mathlib4/pull/14270

[Seewoo Lee]

We are porting our code to mathlib4, and wronskian part is done few days ago. Next step is to port radical, and we upgraded the original definition from polynomial rings to NormalizationMonoid & UniqueFactorizationMonoid, and I wonder where is the best place to put this in mathlib. Note that our radical is different from Ideal.radical - ours is defined as a product of normalized prime factors (hence an element), while later is defined as an ideal.

[Seewoo Lee]

Made PR for the definition of element version of radical, comments are welcome.

[Seewoo Lee]

Here's a PR for another half of the theorems, on radicals of coprime elements (depends on the previous PR). We are considering it as the last "preliminary" PR for our porting - next one would be the last PR containing the proof of the Mason-Stothers theorem.