Erdős Problem 939

Reference: erdosproblems.com/939

def Erdos939Sums (r : ℕ) : Set (Finset ℕ)

A set S belongs to Erdos939Sums r if it meets the following criteria:

• The size of the set is $|S| = r - 2$.
• The elements of the set are coprime (their greatest common divisor is 1).
• Every element in S is an $r$-powerful number.
• The sum of the elements in S, i.e., $\sum_{s \in S} s$, is also an $r$-powerful number.

Equations

• Erdos939Sums r = {S : Finset ℕ | S.card = r - 2 ∧ S.Coprime ∧ r.Full (∑ s ∈ S, s) ∧ ∀ s ∈ S, r.Full s}

theorem erdos_939 : (∀ r ≥ 4, (Erdos939Sums r).Nonempty) ↔ sorry

If $r≥4$ then can the sum of $r-2$ coprime $r$-powerful numbers ever be itself $r$-powerful?

theorem erdos_939.variants.infinite : (∀ r ≥ 4, (Erdos939Sums r).Infinite) ↔ sorry

If $r≥4$ are there infinitely many sums of $r-2$ coprime $r$-powerful numbers that are themselves $r$-powerful?

theorem erdos_939.variants.triples : {(a, b, c) : ℕ × ℕ × ℕ | {a, b, c}.Coprime ∧ Nat.Full 3 a ∧ Nat.Full 3 b ∧ Nat.Full 3 c ∧ a + b = c}.Infinite ↔ sorry

Are there infinitely many triples of coprime $3$-powerful numbers $a, b, c$ such that $a + b = c$?

theorem erdos_939.variants.examples : ∃ r ≥ 4, (Erdos939Sums r).Nonempty

Cambie has found several examples of the sum of $r - 2$ coprime $r$-powerful numbers being itself $r$-powerful. For example when $r=5$ we have $$3761^5=2^8\cdot3^{10}\cdot 5^7 + 2^{12}\cdot 23^6 + 11^5\cdot 13^5$$.

theorem erdos_939.variants.seven : (Erdos939Sums 7).Nonempty

Cambie has also found solutions when $r=7$.

theorem erdos_939.variants.eight : (Erdos939Sums 8).Nonempty

Cambie has also found solutions when $r=8$.

theorem erdos_939.variants.euler : ¬∀ k ≥ 4, ∀ (S : Finset ℕ), S.card = k - 1 → ¬∃ (q : ℕ), ∑ s ∈ S, s ^ k = q ^ k

Euler had conjectured that the sum of $k - 1$ many $k$-th powers is never a $k$-th power, but this is false for $k=5$, as Lander and Parkin [LaPa67] found $$27^5+84^5+110^5+133^5=144^5$$.

[LaPa67] Lander, L. J. and Parkin, T. R., "A counterexample to Euler's sum of powers conjecture." Math. Comp. (1967), 101--103.