Euler's sum of powers conjecture

Conjecture · eulers_sum_of_powers_conjecture

Euler's sum of powers conjecture states that for integers $n > 1$ and $k > 1$ , if the sum of $n$ positive integers each raised to the $k$ -th power equals another integer raised to the $k$ -th power, then $n ≥ k$ .

The conjecture is known to be false for $k = 4$ and $k = 5$ , but remains open for $k ≥ 6$ .

Formal statement · Lean 4.lean

theorem eulers_sum_of_powers_conjecture (n k b : ℕ) (hn : 1 < n) (hk : 5 < k) (a : Fin n → ℕ)
    (ha : ∀ i, a i > 0) (hsum : ∑ i, (a i) ^ k = b ^ k) : k ≤ n := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗