The fourth power folds into a square

A fourth power is a square of a square, so the case of four asks one equation lower down.

Start with a concrete example

2⁴ means squaring 2² again: 16. Likewise 3⁴=81. Their sum 97 is not a square. This checks one example; the theorem must rule out every allowed pair.

A small check: try the idea

Think with the concrete example above. You can try again.

Does 2⁴+3⁴=97 being nonsquare prove the claim for every pair?

Read the answer and reasoning

No; it checks this pair only. 16+81=97 is useful practice, but a universal statement needs an argument covering every allowed pair.

Build the idea in three steps

A fourth power is a square once more: a ^ 4 = (a ^ 2) ^ 2. So a ^ 4 + b ^ 4 = c ^ 4 states exactly (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2 — the same family with the exponent one lower.
The theorem fermatLastTheoremFour states the case directly as FermatLastTheoremFor 4 and immediately rewrites it into the lower form, handing c ^ 2 to not_fermat_42.
So the dossier of this case is a single question: can a ^ 4 + b ^ 4 equal a square c ^ 2 with both a and b non-zero? The answer is no, and the next pages walk the descent that proves it.

A small example

Fold a number into its plainness? Try the small ones: 16 + 81 = 97 — the fourth powers 2⁴ and 3⁴ sum to a number that is not a square, and no other non-zero pair ever succeeds.

Lean definition · original excerpt

Mathlib · db584cd · Four.lean

267theorem fermatLastTheoremFour : FermatLastTheoremFor 4 := by268  rw [fermatLastTheoremFor_iff_int]269  intro a b c ha hb _ heq270  apply @not_fermat_42 _ _ (c ^ 2) ha hb271  rw [heq]; ring

How to read this Lean

rw [fermatLastTheoremFor_iff_int] translates the natural-number statement into integers, carrying the non-zero evidence along. The goal after the rewrite is a ^ 4 + b ^ 4 ≠ (c ^ 2) ^ 2 — exactly the shape not_fermat_42 forbids — and ring closes the small algebraic gap. These five lines carry the whole case: everything else in the file supports not_fermat_42.

Original source ↗ · L267–271 Open the complete saved source

Where this idea is used

7. The veterans’ cabinet

The fourth power folds into a square

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue