Documentation

FormalConjectures.ErdosProblems.«871»

Erdős Problem 871 #

References:

theorem Erdos871.erdos_871 :
False ∀ (A : Set ), ((∀ᶠ (n : ) in Filter.atTop, aA, bA, a + b = n) ∀ (t : ), ∀ᶠ (n : ) in Filter.atTop, ∃ (pairs : Finset ( × )), pairs.card t ppairs, p.1 A p.2 A p.1 + p.2 = n p.1 p.2) → ∃ (B : Set ) (C : Set ), (∀ (x : ), x A x B x C) Disjoint B C (∀ᶠ (n : ) in Filter.atTop, aB, bB, a + b = n) ∀ᶠ (n : ) in Filter.atTop, aC, bC, a + b = n

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.