Erdős Problem 979

Reference: erdosproblems.com/979

def Erdos979.solutionSet (n k : ℕ) : Set (Multiset ℕ)

Equations

• Erdos979.solutionSet n k = {P : Multiset ℕ | P.card = k ∧ (∀ p ∈ P, Nat.Prime p) ∧ n = (Multiset.map (fun (x : ℕ) => x ^ k) P).sum}

theorem Erdos979.erdos_979 : (∀ k ≥ 2, Filter.limsup (fun (n : ℕ) => (solutionSet n k).encard) Filter.atTop = ⊤) ↔ sorry

Let $k ≥ 2$, and let $f_k(n)$ count the number of solutions to $n = p_1^k + \dots + p_k^k$, where the $p_i$ are prime numbers. Is it true that $\limsup f_k(n) = \infty$?

theorem Erdos979.erdos_979_k2 : Filter.limsup (fun (n : ℕ) => (solutionSet n 2).encard) Filter.atTop = ⊤

Erdős [Er37b] proved that if $f_2(n)$ counts the number of solutions to $n = p_1^2 + p_2^2$, where $p_1$ and $p_2$ are prime numbers, then $\limsup f_2(n) = \infty$.

[Er37b] Erdős, Paul, On the Sum and Difference of Squares of Primes. J. London Math. Soc. (1937), 133--136.

theorem Erdos979.erdos_979_k3 : Filter.limsup (fun (n : ℕ) => (solutionSet n 3).encard) Filter.atTop = ⊤

Erdős (unpublished)