Formal target: Corpus.WikipediaEulerSumOfPowers.eulers_sum_of_powers_conjecture

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.

Exact formal statement

∀ (n k b : Nat),
  LT.lt.{0} 1 n →
    LT.lt.{0} 5 k →
      ∀ (a : Fin n → Nat),
        (∀ (i : Fin n), GT.gt.{0} (a i) 0) →
          Eq.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun i => HPow.hPow.{0, 0, 0} (a i) k) (HPow.hPow.{0, 0, 0} b k) →
            LE.le.{0} k n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record