number-theory · diophantine-equations · sums-of-powers
For integers k ≥ 6 and n ≥ 2, let a₁, …, aₙ be positive integers and b a nonnegative integer. If a₁^k + … + aₙ^k = b^k, must n ≥ k? The summands need not be distinct. Positivity makes b = 0 impossible. This is only the k ≥ 6 restriction of Euler’s original conjecture, not the disproved unrestricted statement.
Why it matters
Counterexamples to the original conjecture show why an appealing extrapolation from Fermat’s last theorem needs careful boundaries. The higher-exponent restriction separates an unresolved question from a known false claim.
One possible first attack
First verify the explicit identity 27^5 + 84^5 + 110^5 + 133^5 = 144^5, which lies outside this target. For a modest result inside its range, prove that a sum of two through five sixth powers, with every base coprime to 7, cannot be a sixth power by reducing modulo 7. This is only a restricted obstruction.
Mathematical status
Open restriction, not an open original conjecture (checked 2026-09-11). Euler’s unrestricted assertion is false at k = 4 and k = 5. The supplied target already quantifies only over k > 5; the current reference lists those higher exponents as unresolved. The stronger-looking English description was corrected without changing the target. Do not confuse this with the two-sided Lander–Parkin–Selfridge conjecture.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Current reference distinguishing the disproved original from the unresolved k ≥ 6 restriction (checked 2026-09-11): https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjecture
Meyrignac’s primary computational database: explicit fourth- and fifth-power identities; not a proof of nonexistence (checked 2026-09-11): http://euler.free.fr/
Historical counterexamples and references to Lander–Parkin and Elkies; distinction from two-sided equal-power questions (checked 2026-09-11): https://mathworld.wolfram.com/EulersSumofPowersConjecture.html
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/EulerSumOfPowers.lean
Local target: Corpus.WikipediaEulerSumOfPowers.eulers_sum_of_powers_conjecture
Source SHA-256: 0c42c77344ba4f672f064c04259a21f224a5a64bae019d6d0e06ba47deea809e
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For integers k ≥ 6 and n ≥ 2, let a₁, …, aₙ be positive integers and b a nonnegative integer. If a₁^k + … + aₙ^k = b^k, must n ≥ k? The summands need not be distinct. Positivity makes b = 0 impossible. This is only the k ≥ 6 restriction of Euler’s original conjecture, not the dis
A sum of two through five natural-number sixth powers, with every base not divisible by 7, cannot equal any natural-number sixth power. Only this restricted k = 6 case is proved.
If a sum of n natural-number sixth powers equals a sixth power, and none of the n bases is divisible by 7, then n is congruent to 0 or 1 modulo 7. This is a restricted modular obstruction, not the general Euler conjecture.
A restricted sixth-power obstruction is now Lean-checked. If a_1^6 + ... + a_n^6 = b^6 and none of the bases a_i is divisible by 7, then n is congruent to 0 or 1 modulo 7. Each nonzero residue modulo 7 has sixth power 1, while an arbitrary sixth power is 0 or 1. Reducing the equa