lean_workbook_plus_19750

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

We will prove directly that the equation $x^4 + y^4 = z^2$ has no integer solutions; clearly it suffices to only check for positive integer solutions. Let $(a,b,c)$ be the positive integer solution with smallest $c$ . We note that $a,b,c$ are pairwise relatively prime, because if some prime divided any two variables then it would also divide the third, using $a^4 + b^4 = c^2$ , and we could then divide out this prime to get a smaller $c$ . \n \n So, $a^2$ , $b^2$ , and $c$ are members of a primitive Pythagorean triple. Suppose without loss of generality that $a^2$ is the leg of odd length, so that $a^2 = r^2 - s^2$ , $b^2 = 2rs$ , and $c = r^2 + s^2$ where $r$ and $s$ are relatively prime positive integers of opposite parity. But $a^2 + s^2 = r^2$ , and since $a^2$ is odd, we have $a = m^2 - n^2$ , $s = 2mn$ , and $r = m^2 + n^2$ for relatively prime positive integers $m,n$ of opposite parity. \n \n Now, observe $b^2 = 2rs = 2r(2mn) = 4rmn$ . Notice that $m$ , $n$ , and $r$ are pairwise relatively prime, because if $r$ shared a prime factor with $m$ , this prime would also divide $n$ using $r = m^2 + n^2$ , and similarly for a shared prime factor of $r$ and $n$ . But $m$ and $n$ form a primitive Pythagorean triple, so they are relatively prime. We know $4rmn$ is a square, so in fact $m$ , $n$ , and $r$ are all nonzero perfect squares, say $m = M^2$ , $n = N^2$ , and $r = R^2$ , because they're relatively prime. But $r = m^2 + n^2$ , so $R^2 = M^4 + N^4$ . Also $c = r^2 + s^2$ with $r,s > 0$ , so $r < c$ , hence $R = \sqrt{r} < c$ , and we have produced a smaller solution with smaller $c$ . By infinite descent, we are done.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_19750 : ¬ ∃ x y z : ℤ, x^4 + y^4 = z^2   :=  by sorry

Trivial integer solutions with a zero fourth-power base were not excluded.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

For integers x,y,z with x≠0 and y≠0 prove x⁴+y⁴≠z²; this is the intended nontrivial Fermat fourth-power assertion.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.