search

seewoo5 / lean-poly-abc

Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4
8 stars 0 forks source link

$a^n+b^n+c^n = 0$ and $c^n=a^n+b^n$ FLT versions are slightly different. #12

Closed jcpaik closed 1 year ago

seewoo5 commented 1 year ago

This can be done in the following step:

  1. We only need to consider the cases when n = 4 or n is an odd prime.
  2. For odd prime cases, we can simply consider (-c) instead of c.
  3. For n = 4, I'm quite surprised that I don't know the answer...
seewoo5 commented 1 year ago

Also, the note also consider the Fermat-Catalan equation, which has a form of $a^p + b^q + c^r = 0$. Maybe we can include this too?

jcpaik commented 1 year ago

This can be done in the following step:

  1. We only need to consider the cases when n = 4 or n is an odd prime.
  2. For odd prime cases, we can simply consider (-c) instead of c.
  3. For n = 4, I'm quite surprised that I don't know the answer...

We can write $a^n+b^n+(-c^n)=0$ and apply the Mason's theorem right away. This also deals with n=4. The proof-sketch branch deals with that.

Also, the note also consider the Fermat-Catalan equation, which has a form of ap+bq+cr=0. Maybe we can include this too?

@seewoo5 Do you want to work on this? I will change the main theorem from FLT to FLT-Catalan and sorry out the inequality part in the proof-sketch branch. Maybe you can fill in the rest.