FLT for n=4

Stream: new members

[Rohan Joshi]

Hello everyone, I am taking a small passion project about formalizing the proof of FLT for n=4. I am working in Mathlib, and so far I have gotten the below. The suitable next steps would be to use the solution for the pythagorean triplets to prove our goal. However, I'm not sure how to proceed. Any help would be greatly appreciated!
Screenshot-2024-07-31-at-8.26.23AM.png

[David Michael Roberts]

You need to split into the two cases, no? https://en.wikipedia.org/wiki/Proof_of_Fermat%27s_Last_Theorem_for_specific_exponents#Proof_for_case_A goes straight to the parametrisation of primitive Pythagorean triples, but Case B does some other stuff first (scroll up slightly to see the Case A/B distinction, it's not the same as case I/II.

I guess the big thing you need is the result that prim Pythag triples have their usual parametrisation.

[Rohan Joshi]

Hi, I was using the proof for case A, where upon finding the solutions to the pythagorean triplet, we get another solution. The screenshot below is what I'm referencing for my proof. I'm just not sure what tactics I can use to reach the goal.
Screenshot-2024-07-31-at-12.18.55PM.png

[Notification Bot]

This topic was moved here from #FLT > FLT for n=4 by Riccardo Brasca.

[Riccardo Brasca]

@Rohan Joshi I've moved you message to the #new members stream, since #FLT is specifically about proving the full FLT.

[Riccardo Brasca]

Note that FLT for n=4 is already in mathlib if you want to have a look at how it is done. (It is of course a very nice idea to learn how to write proofs in Lean!)

[Rohan Joshi]

Hi, thank you so much for the referral. However, I'm not sure but is there an easier way to show the formalization for this process?
I'm trying to maintain a relatively simple solution n=4. Is there any solution that follows up on mine?

[Riccardo Brasca]

I think that mathematically mathlib proof is elementary, and probably not very far from what you are proposing. It can be hard to read though. If your goal is to learn Lean you should just go with your proof and ignore mathlib's one, at least at the beginning.