Let $A \subseteq N$ be such that $A + A$ has positive (upper) density. Can one always decompose $A = A_{1} ⊔ A_{2}$ such that $A_{1} + A_{1}$ and $A_{2} + A_{2}$ both have positive (upper) density?Is there a basis $A$ of order $2$ such that if $A = A_{1} ⊔ A_{2}$ then $A_{1} + A_{1}$ and $A_{2} + A_{2}$ cannot both have bounded gaps?

Worked, still open.

additive combinatorics · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

alphaproof · AlphaProof Nexus (DeepMind) · machine-verified (Lean)

Machine-verified Lean proof (kernel-checkable, sorry-free).

Lean proof ↗

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

These are exactly **Erdős Problem #741 (Burr–Erdős)**. As far as I can verify from the literature trail that is commonly cited for this problem, both parts are currently regarded as **open** in full generality. The Erdős Problems site lists the pair of questions as open and notes that Erdős believed he could build an e…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · solved (literature)

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

formal-conjectures/741.lean ↗

Kernel-checked proof; human-attested statement.

faithful — reviewer:will-blair erdos_741.parts.i.lean

status

solved

evidence

formal

status

Search Vela