Erdős Problem 358

References:

• erdosproblems.com/358
• [Ta26] T. Tao, Erdős problem 358 (2026)

def Erdos358.intervalRepresentations (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ)

Equations

• Erdos358.intervalRepresentations A n = {(u, v) : ℕ × ℕ | 0 < u ∧ 0 < v ∧ n = ∑ i ∈ Finset.Icc u v, A i}

noncomputable def Erdos358.f (A : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• Erdos358.f A n = Nat.card ↑(Erdos358.intervalRepresentations A n)

def Erdos358.intervalRepresentationsNonTrivial (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ)

Equations

• Erdos358.intervalRepresentationsNonTrivial A n = {(u, v) : ℕ × ℕ | 0 < u ∧ 0 < v ∧ u < v ∧ n = ∑ i ∈ Finset.Icc u v, A i}

noncomputable def Erdos358.g (A : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• Erdos358.g A n = Nat.card ↑(Erdos358.intervalRepresentationsNonTrivial A n)

theorem Erdos358.f_id : f id = fun (n : ℕ) => {d ∈ n.divisors | Odd d}.card

When $A_n = n$, the function $f$ defined above counts the number of odd divisors of $n$.

theorem Erdos358.erdos_358.parts.i : True ↔ ∃ (A : ℕ → ℕ), StrictMono A ∧ Filter.Tendsto (f A) Filter.atTop Filter.atTop

Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ Is there such an $A$ for which $f(n)\to \infty$ as $n\to \infty$?

Tao [Ta26] constructed such a sequence with $f(n) \gg \log n$ for all sufficiently large $n$.

theorem Erdos358.erdos_358.parts.ii : True ↔ ∃ (A : ℕ → ℕ), StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 2 ≤ f A n

Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ Is there an $A$ such that $f(n)\geq 2$ for all large $n$?

This also follows from Tao's construction with $f(n) \gg \log n$ [Ta26].

theorem Erdos358.erdos_358.variants.prime_set : Filter.limsup (fun (n : ℕ) => ↑(f (Nat.nth Nat.Prime) n)) Filter.atTop = ⊤

When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the $\limsup$ of the number of representations $$n=\sum_{u\leq i\leq v}a_i$$ is infinite.

theorem Erdos358.erdos_358.variants.prime_set_density_representation : 0 < {n : ℕ | (intervalRepresentations (Nat.nth Nat.Prime) n).Nonempty}.upperDensity

When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the set of numbers $n$ that have representations $$n=\sum_{u\leq i\leq v}a_i$$ has positive upper density.

theorem Erdos358.erdos_358.variants.one_le : ∃ (A : ℕ → ℕ), StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ g A n

It is conjectured that if $A =\{a_1 < \cdots\}$ and $g$ counts the number of representations $$n=\sum_{u\leq i\leq v}a_i$$ such that the sum has at least two terms, then for all $n$ we have $1 \leq g(n)$ for sufficiently large $n$.