Skip to content

Erdős problem 741

Start work

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive density in the literal sense that its natural density exists and is positive. Can one always decompose A=A1⊔A2A=A_1\sqcup A_2 such that A1+A1A_1+A_1 and A2+A2A_2+A_2 both have positive density in this sense?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

741.lean

Retained formal statement2 of 4

Is there a basis AA of order 22 such that if A=A1⊔A2A=A_1\sqcup A_2 then A1+A1A_1+A_1 and A2+A2A_2+A_2 cannot both have bounded gaps?

This was proved by DeepMind prover agent.

FormalConjectures/ErdosProblems/741.leanErdos741.erdos_741.parts.ii4 linesExact file
True ↔  ∃ A,    (A ∪ {0}).IsAddBasisOfOrder 2 ∧      ∀ (A₁ A₂ : Set ℕ), A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂))
SolvedProof has a holeformal conjecturesexternal proof

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