Fermat's last theorem for exponent 4

[icecream17]

Draft since I'm avoiding a merge conflict (deduction of opthpr will be where ifexd was: #4139), but everything is proved except for the lemmas Done

In changes-set.txt I replaced two tabs with spaces fixed by #4160

Edit: flt4lem5 is impossible to prove. flt4g will become a lemma with an extra A < B hypothesis, and flt4 will become nontrivial (will use fltne)...

edit 2: A < B is not very useful considering the relevant terms are A ^ 4 and B ^ 2, so instead the parity antecedent from pythagtriplem18 will be carried over

edit 3: A better proof was used

[metakunt]

Nice, how much harder is exponent 3?

[icecream17]

FLT3 seems several times as hard as FLT4, judging by https://en.wikipedia.org/wiki/Proof_of_Fermat%27s_Last_Theorem_for_specific_exponents#n_=_3 (though it uses a "crucial lemma" without proving it)

and Lean, which has tactics and probably a better library given its cyclotomic Three import, and which takes 600 lines to prove FLT3
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/FLT/Three.lean

worse options I looked at

I tried to find if anyone found a simple proof, but to no avail.

---

https://www.researchgate.net/publication/269238745_Proof_of_Fermat's_Last_Theorem_for_n3_Using_Tschirnhaus_Transformation
has many steps introducing very complicated substitutions and transformations, ending with

then

Which I find rather amusing. Other than the slightly questionable last sentence, it does not seem wrong, but it also does not seem to have garnered any citations.

---

Strangely, google keeps shoving the one vixra paper, which obviously doesn't work (edit: ironic typo). But there's also this arxiv paper: https://arxiv.org/abs/math/0309005 which is wrong because the logic at the end of page 6 doesn't connect (I can't tell what "embedded" means, based on the second last paragraph on page 6 it means two groups of equations can be true at the same time. That would make page 6 last paragraph sentence 2 equivalent to FLT, however the proof of that sentence is not given).

Afaict no one has bothered to refute this paper until now, probably because the grammar + the claim was a red flag.

[metakunt]

What do you mean by questionable? The proof appears to be short to be formalised.
Is there any step that is likely a non-sequitur?

[icecream17]

I was referring to "...and thereby this proof suggests that there is a possibility of existence of a simple proof to the Fermat's Last Theorem in general", there doesn't seem to be anything wrong with the actual proof.

[metakunt]

So formalising FLT for n=3 is in reach? I think we might even have Cardano in set.mm

[avekens]

Very interesting (intermediate) results, and nice generalizations of existing theorems. Please go ahead.

[icecream17]

More delays: I just rediscovered my notes which links to a proof that's even better than wikipedia's

[benjub]

General note: for these theorems, I think the following statements look nicer:

( ph -> A e. ZZ) 
...
( ph -> ( ( A ^ 4  ) + ( B ^ 4 ) ) =  ( C ^ 2 ) )
=>
( ph -> ( A x B ) =  0 )

And when the exponent is odd, the conclusion is ( ph -> ( ( A x B ) x C ) = 0 ) (or associated the other way, I do not know which we prefer in set.mm)

[icecream17]

Almost done, except for proving a lemma, flt4g modified, and flt4g (new label)

Here's what the new a1ii looks like. I converted the text into a list, used <code> for commands, and added the sentence below it (I highlighted the first word).

[benjub]

This looks prettier indeed, and this change is good to me. As a loose principle, I think there are two things to be wary of:

• do not spend too much time on rich formatting of comments since the further we depart from plain text, the harder the database is to maintain (but of course, when necessary for improving understanding, do use available functionalities);
• if there are general instructions or remarks about "proof engineering" which are not specific to set.mm, they probably have a better place to be that in set.mm.

Again, I think that in the current case this is ok (even though the method with using a1ii is generalizable to various sorts of databases, and these general guidelines could be added somewhere more general).

[benjub]

Cosmetic, but the order of hypotheses is not very natural (same in next theorem): why not first K, M, N integers, and then the two divisibility hypotheses?
It is important to have uniform "APIs".

[tirix]

Those K e. ZZ, M e. ZZ and N e. ZZ are even actually redundant by dvdszrcl

[benjub]

@tirix do you think we could discourage that theorem ? For instance as an "implementation detail", or "too fragile" (e.g., if in the future we want to extend it, for instance as in https://us.metamath.org/mpeuni/df-bj-divc.html).

In every textbook, similar statements about divisibility begin with "Let K, M, N be integers".

[tirix]

@tirix do you think we could discourage that theorem ?

Oh, I see. Yes, why not ?

[benjub]

Or maybe:

Move a subtraction in the RHS to a right-addition in the LHS.

[benjub]

Same kind of things: it seems strange to "swap" the whole LHS with a part of the RHS.

Move a right-addition to in the RHS to a subtraction in the LHS, and then use symmetry of equality.

Same for the following results.

[benjub]

As you proved in the theorem above, N can be in NN0. Also, C can be in ZZ, and maybe A and B too.

It would certainly be nice to be as general as possible, but it may be a bit annoying in the proofs. Hopefully the generalization of the earlier results to ZZ will reduce the needs to treat zero separately.

The same questions will appear repeatedly below. Since it is in your mathbox, these are non-blocking remarks.

[tirix]

Maybe it's possible (easier) to first keep the proof in NN as a kind of lemma, and then extend to ZZ in a subsequent proof?

[benjub]

@tirix It may be. I cannot tell from here: it really depends on whether zero has to be treated separately in specific subproofs, or if there is no need for it because the above lemmas have been properly generalized.

[icecream17]

The theorems currently depend on ~ dvdsexpnn (this pr) to go from ? || ( ? ^ N ) to ? || ?

~ dvdsexpnn is comparable with ~ dvdssqlem , and as seen from ~ dvdssq the generalization is not free, though it would be nice. TODO-SNd to later

[tirix]

I was thinking using theorems like neggcd, gcdneg, negdvdsb and dvdsnegb to fall back to positive integers. Similar theorems can be used to treat the zero cases.

[icecream17]

Note: The force push only changes the commit message to link to a more relevant pr

[icecream17]

I think this is equivalent to a non-draft state, although #4149 (comment) isn't resolved yet

[benjub]

Good for me, even if I have one labeling remark (see "rotate" above), and I hope that in the future, as many of these statements as possible will have more general and natural hypotheses, typically, A, B, C \in \ZZ (and exponent in \NN0 when the statement remains true without complicating it, or else \NN), and expressing triviality of solutions by ABC=0. That is, statements of the form:

All solutions in $\mathbb{Z}^d$ to [this or that Diophantine equation] are trivial.

rather than

[This or that Diophantine equation] has no solution in [this or that subset of $\mathbb{Z}^d$].

[benjub]

I gave my approval above (and hopefully my comment to the approval will be useful). There are two other reviewers, @tirix and @avekens. Good for you? Feel free to merge if so.

[icecream17]

if you are referring to me, I do not have merge permissions

[benjub]

if you are referring to me, I do not have merge permissions

I was referring to Thierry and Alexander (the requested reviewers are displayed at the top of the right pane on this page).

[tirix]

No objections from me!