Sums of consecutive terms of a sequence

DefinitionInterval-sum representation count#✓fully proved

For a sequence \(a_0, a_1, a_2, \ldots\) of natural numbers and a natural number \(n\), \(f_a(n)\) is the number of pairs \((u, v)\) of natural numbers with \(u \le v\) and \(a_u + a_{u+1} + \cdots + a_v = n\), and \(f_a(n) = 0\) if there are infinitely many such pairs.

The sequence is indexed from \(0\) rather than from \(1\) as in the source; this does not change the count. When the sequence is strictly increasing with positive terms there are only finitely many such pairs, so \(f_a(n)\) is then the true number of representations.

noncomputable def RepCount (A : ℕ → ℕ) (n : ℕ) : ℕ :=
  Nat.card {(p : ℕ × ℕ) | p.1 ≤ p.2 ∧ (∑ i ∈ Finset.Icc p.1 p.2, A i) = n}

Used by 1

Used byThe interval-sum conjecture of Erdős Problem 358

DefinitionThe interval-sum conjecture of Erdős Problem 358#✓fully proved

This is the proposition that there is a strictly increasing sequence \(a_0 < a_1 < a_2 < \cdots\) of positive integers whose interval-sum representation count \(f(n)\), the number of pairs \((u, v)\) of natural numbers with \(u \le v\) and \(a_u + a_{u+1} + \cdots + a_v = n\), tends to infinity as \(n \to \infty\).

def conjecture : Prop :=
  ∃ A : ℕ → ℕ, StrictMono A ∧ 0 < A 0 ∧
    Filter.Tendsto (fun n : ℕ => RepCount A (n : ℕ)) Filter.atTop Filter.atTop

Uses 1 · Used by 1

Statement usesInterval-sum representation count

Used byInterval sums with unbounded representation counts (Erdős Problem 358)

TheoremInterval sums with unbounded representation counts (Erdős Problem 358)#●ready to prove

There is a strictly increasing sequence \(a_0 < a_1 < a_2 < \cdots\) of positive integers such that the number \(f(n)\) of pairs \((u, v)\) of natural numbers with \(u \le v\) and \(a_u + a_{u+1} + \cdots + a_v = n\) tends to infinity as \(n \to \infty\).

Resolved true: Resolved by Tao's February 2026 construction of a set A of positive integers with f(n) >> log n for all large n, hence f(n) -> infinity (Erdos Problems record 358, [Ta26]).

public theorem_wanted conjecture_holds : conjecture

Sources

• Terence Tao, construction of a set A of positive integers with f(n) >> log n for Erdos Problem 358, February 2026, https://terrytao.wordpress.com/wp-content/uploads/2026/02/erdos-358-2.pdf.

Uses 1

Statement usesThe interval-sum conjecture of Erdős Problem 358

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.