# Proof: There are no positive integer solutions to the equation x^4 + y^4 = z^4.

- **Generated:** 2026-03-28
- **Verdict:** UNDETERMINED
- **Audit trail:** [proof_audit.md](proof_audit.md) | [proof.py](proof.py)

## Key Findings

- Exhaustive search over all positive integers x, y, z in [1, 1000] found **zero solutions** to x^4 + y^4 = z^4 (A1).
- An independent subtraction-based algorithm confirmed zero solutions over the same range (A2).
- Modular analysis (mod 16) proves that both x and y cannot be odd in any solution, providing independent structural constraints (A3).
- The claim is a proven theorem (Fermat, c. 1637; also implied by Wiles' 1995 proof of FLT), but the infinite descent argument cannot be machine-verified, so the verdict is **UNDETERMINED** per proof-engine conventions.

## Claim Interpretation

**Natural language:** There are no positive integer solutions to the equation x^4 + y^4 = z^4.

**Formal interpretation:** The number of positive integer triples (x, y, z) with x, y, z >= 1 satisfying x^4 + y^4 = z^4 equals zero.

**Operator rationale:** The claim asserts zero solutions exist. A single counterexample would disprove it. This is Fermat's Last Theorem for n=4, proved by Fermat via infinite descent. The computational verification covers a finite range [1, 1000]; the full proof for all integers relies on infinite descent which is documented as prose but not machine-verified.

## Evidence Summary

| ID | Fact | Verified |
|----|------|----------|
| A1 | Exhaustive search: no solutions with x,y,z in [1, 1000] | Computed: 0 solutions found in [1, 1000] via addition-based search |
| A2 | Independent cross-check: subtraction method confirms no solutions in [1, 1000] | Computed: 0 solutions found via independent subtraction-based algorithm |
| A3 | Modular analysis: fourth-power residues mod 16 constrain solutions | Computed: True (both-odd case eliminated; fourth-power residues mod 16 are {0, 1}) |

*Source: proof.py JSON summary*

## Proof Logic

The proof approaches the claim from three independent angles:

**Exhaustive search (A1):** For every pair (x, y) with 1 <= x <= y <= 1000, compute x^4 + y^4 and check whether the sum is a perfect fourth power using integer arithmetic (avoiding floating-point errors). Zero solutions were found across all 500,500 pairs tested.

**Subtraction-based cross-check (A2):** Using an algorithmically independent method, for every z in [2, 1000] and x in [1, z-1], compute z^4 - x^4 and check if the remainder is a positive perfect fourth power. This subtraction-based approach independently confirmed zero solutions, agreeing with A1.

**Modular analysis (A3):** Fourth powers modulo 16 can only be 0 or 1. Therefore x^4 + y^4 mod 16 can be 0, 1, or 2. Since z^4 mod 16 must be 0 or 1, the case where both x and y are odd (producing residue 2) is impossible. This provides an independent structural constraint consistent with zero solutions.

**Classical proof (not machine-verified):** Fermat's infinite descent proof (c. 1637) proves the stronger result that x^4 + y^4 = z^2 has no positive integer solutions. Since z^4 is a perfect square, x^4 + y^4 = z^4 has no solutions either. The descent argument assumes a minimal solution exists and derives a strictly smaller one, contradicting the well-ordering principle. This argument covers all positive integers but cannot be machine-verified by this engine.

## Counter-Evidence Search

- **Known counterexamples or disputes?** Fermat's proof for n=4 is universally accepted in mathematics. Euler gave an independent proof. The result also follows from Wiles' 1995 proof of Fermat's Last Theorem for all n >= 3. No counterexample has ever been found.
- **Large solutions beyond the bound?** The infinite descent argument guarantees no solutions at any scale. Computational searches have verified FLT for n=4 to at least 10^18.
- **Solutions in other number systems?** Real solutions exist trivially (e.g., x=y=1, z=2^(1/4)), but the claim is about positive integers. No rational solutions exist either.

*Source: proof.py JSON summary*

## Conclusion

**Verdict: UNDETERMINED**

Exhaustive computational search over [1, 1000] found zero solutions to x^4 + y^4 = z^4 (A1), confirmed by an independent algorithm (A2). Modular analysis provides additional structural constraints (A3). The claim is mathematically true — it is Fermat's Last Theorem for n=4, proved by Fermat via infinite descent (c. 1637) and independently by Euler, and also a corollary of Wiles' 1995 proof of FLT. However, the infinite descent argument is a logical chain that cannot be machine-verified by this engine. Per proof-engine conventions, claims on infinite domains whose proofs rely on unverified logical steps receive an UNDETERMINED verdict. The computational evidence strongly supports the claim up to the verified bound.

---

Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v0.10.0 on 2026-03-28.