Erdős problem 871 · problems.science

Let $A$ be an additive basis of order $2$ , and suppose $1_A\ast 1_A(n)\to \infty$ as $n\to \infty$ . Can $A$ be partitioned into two disjoint additive bases of order $2$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

871.lean

Retained formal statement1 of 1

Let $A$ be an additive basis of order $2$ , and suppose $1_A\ast 1_A(n)\to \infty$ as $n\to \infty$ . Can $A$ be partitioned into two disjoint additive bases of order $2$ ?

A question of Erdős and Nathanson [ErNa88], who proved this is true if $1_A\ast 1_A(n) > c\log n$ (for all large $n$ ) for some constant $c>(\log\frac{4}{3})^{-1}$ . Erdős and Nathanson [ErNa89] also proved that for every $t$ there exists a basis $A$ of order $2$ such that $1_A\ast 1_A(n)\geq t$ for all large $n$ and yet $A$ cannot be partitioned into two disjoint additive bases. This has been disproved by Larsen using Claude Opus 4.5 - in fact only a small modification of the argument of [ErNa89] is required.

FormalConjectures/ErdosProblems/871.leanErdos871.erdos_87111 linesExact file

1False ↔2  ∀ (A : Set ℕ),3    ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧4        ∀ (t : ℕ),5          ∀ᶠ (n : ℕ) in Filter.atTop,6            ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) →7      ∃ B C,8        (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧9          Disjoint B C ∧10            (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧11              ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science