Erdős Problem 741

References:

• erdosproblems.com/741
• [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.

theorem Erdos741.erdos_741.parts.i : False ↔ ∀ (A : Set ℕ), (A + A).HasPosDensity → ∃ (A₁ : Set ℕ) (A₂ : Set ℕ), A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ (A₁ + A₁).HasPosDensity ∧ (A₂ + A₂).HasPosDensity

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density?

Note that this is using a literal interpretation of "positive density".

This was disproved by the DeepMind prover agent.

theorem Erdos741.erdos_741.variants.lower : True ↔ ∀ (A : Set ℕ), 0 < (A + A).lowerDensity → ∃ (A₁ : Set ℕ) (A₂ : Set ℕ), A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).lowerDensity ∧ 0 < (A₂ + A₂).lowerDensity

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive lower density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive lower density?

theorem Erdos741.erdos_741.variants.upper : True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ (A₁ : Set ℕ) (A₂ : Set ℕ), A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive upper density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive upper density?

theorem Erdos741.erdos_741.parts.ii : True ↔ ∃ (A : Set ℕ), (A ∪ {0}).IsAddBasisOfOrder 2 ∧ ∀ (A₁ A₂ : Set ℕ), A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂))

Is there a basis $A$ of order $2$ such that if $A=A_1\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?

This was proved by DeepMind prover agent.