Formal target: Corpus.WikipediaLanderParkinAndSelfridgeConjecture.lander_parkin_selfridge
The Lander–Parkin–Selfridge conjecture: if the sum of $n$ positive integer $k$-th powers equals the sum of $m$ positive integer $k$-th powers, with all values on the left distinct from all values on the right, then $n + m \geq k$.
Exact formal statement
∀ (k n m : Nat) (x : Fin n → Nat) (y : Fin m → Nat),
LT.lt.{0} 0 n →
LT.lt.{0} 0 m →
(∀ (i : Fin n), LT.lt.{0} 0 (x i)) →
(∀ (i : Fin m), LT.lt.{0} 0 (y i)) →
(∀ (i : Fin n) (j : Fin m), Ne.{1} (x i) (y j)) →
Eq.{1} (Finset.sum.{0, 0} Finset.univ.{0} fun i => HPow.hPow.{0, 0, 0} (x i) k)
(Finset.sum.{0, 0} Finset.univ.{0} fun j => HPow.hPow.{0, 0, 0} (y j) k) →
LE.le.{0} k (HAdd.hAdd.{0, 0, 0} n m)This target is a formal statement, not a proof of the problem.
Environment availability: available.