Existing in Mathlib · Number theory
Fermat's Last Theorem for Exponent Four
No three nonzero natural numbers a, b, and c satisfy a⁴ + b⁴ = c⁴.
- Fermat's Last Theorem
- exponent four
- Diophantine equations
- infinite descent
- minimal counterexamples
- primitive Pythagorean triples
Exact theorem
Exact Mathlib statement
theorem fermatLastTheoremFour : FermatLastTheoremFor 4The theorem at a glance
Fermat's Last Theorem for Exponent Four — infinite descent
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Fermat's Last Theorem for Exponent Four — infinite descent
Detailed visual description
The poster centers the exact nonzero-natural conclusion a⁴+b⁴≠c⁴. Below it, an unlabeled engraved square construction shrinks through two successive right-triangle decompositions. A compact stronger-equation panel and five-step route explain the least-counterexample contradiction while the footer limits the result to exponent four.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Exponent-four descent below a minimal configuration — scientific schematic
Detailed visual description
Large cobalt and emerald gridded square motifs meet in a right-triangle construction. The same geometry recurs at successively smaller scales along a single gold curve, representing the least-versus-smaller conflict used in the exponent-four descent. The figure contains no equation and does not claim the full Fermat's Last Theorem, an exponent-general result, or a finite search.
Why it matters
A mathematical landmark
The exponent-four case is a classical landmark in Diophantine analysis: a minimal hypothetical solution to a stronger square equation is transformed into a smaller one, giving a canonical example of infinite descent.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's theorem FermatLastTheoremFor 4. Unfolded, for natural numbers a, b, and c, if all three are nonzero then a ^ 4 + b ^ 4 ≠ c ^ 4. The source proves this through a stronger integer square equation and infinite descent. The declaration is the exponent-four case only, not full Fermat's Last Theorem, an exponent-general theorem, or new ProofAtlas mathematics.
- The checked declaration proves the case n = 4 only; it does not prove Fermat's Last Theorem for every exponent.
- The exact statement is over natural numbers and assumes that a, b, and c are all nonzero.
- The stronger integer equation a ^ 4 + b ^ 4 = c ^ 2 is the source's proof route, not an expansion of the declaration's public statement.
- The theorem is an impossibility result; it does not enumerate solutions, provide a finite search bound, or assert a computational method.
- ProofAtlas is indexing an existing Mathlib theorem, not claiming mathematical novelty.
Source and local evidence
Where the theorem comes from
- Existing declaration
fermatLastTheoremFourin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.fermat-last-theorem-exponent-four.v001