Splitting sets with dense sumsets

DefinitionErdős Problem 741, upper-density question#✓fully proved

This proposition asserts that for every set \(A \subseteq \mathbb{N}\) whose sumset \(A + A = \{a + b : a, b \in A\}\) has positive upper density there are disjoint sets \(A_1, A_2 \subseteq \mathbb{N}\) with \(A_1 \cup A_2 = A\) such that both \(A_1 + A_1\) and \(A_2 + A_2\) have positive upper density.

def upperDensitySumsetSplits : Prop :=
  ∀ A : Set ℕ, 0 < (A + A).upperDensity → ∃ A₁ A₂ : Set ℕ, Disjoint A₁ A₂ ∧ A₁ ∪ A₂ = A ∧
    0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

Uses 1 · Used by 1

Statement usesUpper density

Used bySplitting a set whose sumset has positive upper density

DefinitionSets with bounded gaps#✓fully proved

A set \(S \subseteq \mathbb{N}\) has bounded gaps (is syndetic) if there is a natural number \(g\) such that for every natural number \(n\) some \(s \in S\) satisfies \(n \le s < n + g\).

def HasBoundedGaps (S : Set ℕ) : Prop :=
  ∃ g : ℕ, ∀ n : ℕ, ∃ s ∈ S, n ≤ s ∧ s < n + g

Used by 1

Used byErdős Problem 741, bounded-gaps question

DefinitionErdős Problem 741, bounded-gaps question#✓fully proved

This proposition asserts that there is a set \(A \subseteq \mathbb{N}\) that is an asymptotic additive basis of order \(2\) (all but finitely many natural numbers are sums of two elements of \(A\)) such that for all disjoint sets \(A_1, A_2 \subseteq \mathbb{N}\) with \(A_1 \cup A_2 = A\), the sumsets \(A_1 + A_1 = \{a + b : a, b \in A_1\}\) and \(A_2 + A_2\) do not both have bounded gaps.

def basisWithoutBoundedGapSplit : Prop :=
  ∃ A : Set ℕ, A.IsAsymptoticAddBasisOfOrder 2 ∧
    ∀ A₁ A₂ : Set ℕ, Disjoint A₁ A₂ → A₁ ∪ A₂ = A →
      ¬ (HasBoundedGaps (A₁ + A₁) ∧ HasBoundedGaps (A₂ + A₂))

Uses 2 · Used by 1

Statement usesSets with bounded gaps · Asymptotic additive basis of order \(n\)

Used byAn asymptotic basis of order 2 admitting no bounded-gap splitting

TheoremSplitting a set whose sumset has positive upper density#●ready to prove

For every set \(A \subseteq \mathbb{N}\) whose sumset \(A + A = \{a + b : a, b \in A\}\) has positive upper density, there are disjoint sets \(A_1, A_2 \subseteq \mathbb{N}\) with \(A_1 \cup A_2 = A\) such that both \(A_1 + A_1\) and \(A_2 + A_2\) have positive upper density.

public theorem_wanted upperDensitySumsetSplits_holds : upperDensitySumsetSplits

Sources

• T. F. Bloom, Erdős Problems, Problem #741, https://www.erdosproblems.com/741 (status SOLVED (LEAN)); resolution: B. Alexeev, M. Putterman, M. Sawhney, M. Sellke and G. Valiant, Short proofs in combinatorics and number theory, arXiv:2603.29961 (2026); erdosproblems.com/741 (DeepMind), Theorem 3.1 of arXiv:2603.29961 (proof due to an internal OpenAI model): there is A ⊂ ℕ, a basis of order 2 with [4, ∞) ⊆ A + A, such that for every partition A = A₁ ⊔ A₂ one of A₁ + A₁, A₂ + A₂ does not have bounded gaps; erdosproblems.com/741: DeepMind gave a positive answer to the upper-density question (proof sketched in the comments), https://arxiv.org/abs/2603.29961.

Uses 1

Statement usesErdős Problem 741, upper-density question

TheoremAn asymptotic basis of order 2 admitting no bounded-gap splitting#●ready to prove

There is a set \(A \subseteq \mathbb{N}\) that is an asymptotic additive basis of order \(2\) (all but finitely many natural numbers are sums of two elements of \(A\)) such that for all disjoint sets \(A_1, A_2 \subseteq \mathbb{N}\) with \(A_1 \cup A_2 = A\), the sumsets \(A_1 + A_1 = \{a + b : a, b \in A_1\}\) and \(A_2 + A_2\) do not both have bounded gaps, where a set \(S \subseteq \mathbb{N}\) has bounded gaps if for some \(g \in \mathbb{N}\) every interval \([n, n + g)\) with \(n \in \mathbb{N}\) meets \(S\).

public theorem_wanted basisWithoutBoundedGapSplit_holds : basisWithoutBoundedGapSplit

Sources

• T. F. Bloom, Erdős Problems, Problem #741, https://www.erdosproblems.com/741 (status SOLVED (LEAN)); resolution: B. Alexeev, M. Putterman, M. Sawhney, M. Sellke and G. Valiant, Short proofs in combinatorics and number theory, arXiv:2603.29961 (2026); erdosproblems.com/741 (DeepMind), Theorem 3.1 of arXiv:2603.29961 (proof due to an internal OpenAI model): there is A ⊂ ℕ, a basis of order 2 with [4, ∞) ⊆ A + A, such that for every partition A = A₁ ⊔ A₂ one of A₁ + A₁, A₂ + A₂ does not have bounded gaps; erdosproblems.com/741: DeepMind gave a positive answer to the upper-density question (proof sketched in the comments), https://arxiv.org/abs/2603.29961.

Uses 1

Statement usesErdős Problem 741, bounded-gaps question

DefinitionErdős Problem 871 (splitting rich bases of order 2)#✓fully proved

The statement that for every set \(A\) of natural numbers such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in A\) and, for every natural number \(t\), every sufficiently large \(n\) has at least \(t\) representations \(n = a + b\) with \(a, b \in A\) and \(a \le b\), the set \(A\) is the disjoint union of two sets \(B\) and \(C\) such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in B\) and every sufficiently large \(n\) is \(a + b\) with \(a, b \in C\).

def conjecture : Prop :=
  ∀ (A : Set ℕ),
    (∀ᶠ n in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧
    (∀ t, ∀ᶠ n in Filter.atTop, ∃ pairs : Finset (ℕ × ℕ),
      pairs.card ≥ t ∧
        ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) →
    ∃ (B C : Set ℕ),
      (∀ x, x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧
      Disjoint B C ∧
      (∀ᶠ n in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧
      (∀ᶠ n in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n)

Used by 2

Used byErdős Problem 871 is false (Larsen) · Negation of the Erdős Problem 871 statement

DefinitionNegation of the Erdős Problem 871 statement#✓fully proved

This is the proposition that there is a set \(A\) of natural numbers such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in A\) and, for every natural number \(t\), every sufficiently large \(n\) has at least \(t\) representations \(n = a + b\) with \(a, b \in A\) and \(a \le b\), but \(A\) is not the disjoint union of two sets \(B\) and \(C\) such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in B\) and every sufficiently large \(n\) is \(a + b\) with \(a, b \in C\).

def disprovedForm : Prop := ¬ conjecture

Uses 1

Statement usesErdős Problem 871 (splitting rich bases of order 2)

TheoremErdős Problem 871 is false (Larsen)#●ready to prove

There is a set \(A\) of natural numbers such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in A\) and, for every natural number \(t\), every sufficiently large \(n\) has at least \(t\) representations \(n = a + b\) with \(a, b \in A\) and \(a \le b\), but \(A\) is not the disjoint union of two sets \(B\) and \(C\) such that every sufficiently large \(n\) is \(a + b\) with \(a, b \in B\) and every sufficiently large \(n\) is \(a + b\) with \(a, b \in C\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Larsen (formalized in Lean), per erdosproblems.com/871, https://www.erdosproblems.com/871; Lean disproof of Erdos Problem 871 (Larsen with Claude Opus 4.5), plby/lean-proofs, https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos871.lean#L2388.

Uses 1

Statement usesErdős Problem 871 (splitting rich bases of order 2)

5 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.