Euler's sum of powers conjecture

Reference: Wikipedia

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

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 \geq k$.

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

theorem EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k4 : ¬∀ (n b : ℕ), 1 < n → ∀ (a : Fin n → ℕ), (∀ (i : Fin n), a i > 0) → ∑ i : Fin n, a i ^ 4 = b ^ 4 → 4 ≤ n

theorem EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k5 : ¬∀ (n b : ℕ), 1 < n → ∀ (a : Fin n → ℕ), (∀ (i : Fin n), a i > 0) → ∑ i : Fin n, a i ^ 5 = b ^ 5 → 5 ≤ n