Asymptotic additive bases

DefinitionAsymptotic additive basis of order \(n\)#✓fully proved

Let \(M\) be an additive commutative monoid, \(A \subseteq M\) and \(n\) a natural number. \(A\) is an asymptotic additive basis of order \(n\) if all but finitely many elements of \(M\) are sums of exactly \(n\) (not necessarily distinct) elements of \(A\), that is, \(M \setminus nA\) is finite, where \(nA = \{a_1 + \dots + a_n : a_1, \dots, a_n \in A\}\) and \(0A = \{0\}\).

For \(M = \mathbb{N}\) this means that every sufficiently large natural number is such a sum.

def IsAsymptoticAddBasisOfOrder (A : Set M) (n : ℕ) : Prop :=
  ∀ᶠ a in cofinite, a ∈ n • A

Used by 2

Used byAsymptotic additive basis · Erdős Problem 741, bounded-gaps question

DefinitionExact additive basis of order \(n\)#✓fully proved

Let \(M\) be an additive commutative monoid, \(A \subseteq M\) and \(n\) a natural number. \(A\) is an exact additive basis of order \(n\) if every element of \(M\) is a sum of exactly \(n\) (not necessarily distinct) elements of \(A\), that is, \(M = nA\), where \(nA = \{a_1 + \dots + a_n : a_1, \dots, a_n \in A\}\) and \(0A = \{0\}\).

def IsAddBasisOfOrder (A : Set M) (n : ℕ) : Prop := ∀ a, a ∈ n • A

DefinitionAsymptotic additive basis#✓fully proved

A subset \(A\) of an additive commutative monoid \(M\) is an asymptotic additive basis if there is a natural number \(n\) such that \(A\) is an asymptotic additive basis of order \(n\), that is, all but finitely many elements of \(M\) are sums of exactly \(n\) (not necessarily distinct) elements of \(A\).

def IsAsymptoticAddBasis (A : Set M) : Prop := ∃ n, A.IsAsymptoticAddBasisOfOrder n

Uses 1

Statement usesAsymptotic additive basis of order \(n\)

DefinitionWeak additive basis of order \(n\)#✓fully proved

Let \(M\) be an additive commutative monoid, \(A \subseteq M\) and \(n\) a natural number. \(A\) is a weak additive basis of order \(n\) if every element of \(M\) is a sum of at most \(n\) (not necessarily distinct) elements of \(A\), that is, lies in \(mA\) for some \(m \le n\), where \(mA = \{a_1 + \dots + a_m : a_1, \dots, a_m \in A\}\) and \(0A = \{0\}\).

def IsWeakAddBasisOfOrder (A : Set M) (n : ℕ) : Prop := ∀ a, ∃ m ≤ n, a ∈ m • A

Used by 1

Used byWeak additive basis

DefinitionWeak additive basis#✓fully proved

A subset \(A\) of an additive commutative monoid \(M\) is a weak additive basis if there is a natural number \(n\) such that \(A\) is a weak additive basis of order \(n\), that is, every element of \(M\) is a sum of at most \(n\) (not necessarily distinct) elements of \(A\).

def IsWeakAddBasis (A : Set M) : Prop := ∃ n, A.IsWeakAddBasisOfOrder n

Uses 1

Statement usesWeak additive basis of order \(n\)

DefinitionSumset of a set of naturals#✓fully proved

For a set \(A\) of natural numbers, \(A + A\) is the set of natural numbers \(n\) such that \(n = a + b\) for some \(a, b \in A\).

def addSumset (A : Set ℕ) : Set ℕ :=
  { n | ∃ a ∈ A, ∃ b ∈ A, a + b = n }

Used by 1

Used byMinimal additive basis of order 2

DefinitionAdditive basis of order 2#✓fully proved

A set \(A\) of natural numbers is an additive basis of order \(2\) if there is a natural number \(N\) such that every natural number \(n \ge N\) can be written as \(n = a + b\) with \(a, b \in A\).

def IsAdditiveBasisOrder2 (A : Set ℕ) : Prop :=
  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ a ∈ A, ∃ b ∈ A, a + b = n

Used by 2

Used byMinimal additive basis of order 2 · Erdős Problem 869 (disjoint bases and minimal bases)

DefinitionMinimal additive basis of order 2#✓fully proved

A set \(A\) of natural numbers is a minimal additive basis of order \(2\) if it is an additive basis of order \(2\) and, for every \(a \in A\), infinitely many natural numbers do not lie in the sumset \((A \setminus \{a\}) + (A \setminus \{a\})\).

def IsMinimalAdditiveBasisOrder2 (A : Set ℕ) : Prop :=
  IsAdditiveBasisOrder2 A ∧ ∀ a ∈ A, ((addSumset (A \ {a}))ᶜ).Infinite

Uses 2 · Used by 1

Statement usesAdditive basis of order 2 · Sumset of a set of naturals

Used byErdős Problem 869 (disjoint bases and minimal bases)

DefinitionErdős Problem 869 (disjoint bases and minimal bases)#✓fully proved

The statement that for all disjoint sets \(A_1\) and \(A_2\) of natural numbers that are both additive bases of order \(2\), there is a set \(B \subseteq A_1 \cup A_2\) that is a minimal additive basis of order \(2\).

def Statement : Prop :=
  ∀ A1 A2 : Set ℕ, Disjoint A1 A2 → IsAdditiveBasisOrder2 A1 →
    IsAdditiveBasisOrder2 A2 →
    ∃ B : Set ℕ, B ⊆ A1 ∪ A2 ∧ IsMinimalAdditiveBasisOrder2 B

Uses 2 · Used by 1

Statement usesAdditive basis of order 2 · Minimal additive basis of order 2

Used byErdős Problem 869 is false (Larsen)

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

There are disjoint sets \(A_1\) and \(A_2\) of natural numbers, both additive bases of order \(2\), such that no subset of \(A_1 \cup A_2\) is a minimal additive basis of order \(2\).

public theorem_wanted Statement_refuted : ¬ Statement

Sources

• Daniel Larsen, Three questions of Erdős–Nathanson on asymptotic bases of order 2, arXiv:2603.03472 (2026), https://arxiv.org/abs/2603.03472; Lean proof of the negative answer to Erdős Problem 869, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos869.lean#L3490.

Uses 1

Statement usesErdős Problem 869 (disjoint bases and minimal bases)

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.