Skip to content

Erdős problem 871

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/871.lean

Formal Conjectures

FormalConjectures/ErdosProblems/871.leanErdos871.erdos_87111 linesExact file
False ↔  ∀ (A : Set ℕ),    ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧        ∀ (t : ℕ),          ∀ᶠ (n : ℕ) in Filter.atTop,            ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) →      ∃ B C,        (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧          Disjoint B C ∧            (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧              ∀ᶠ (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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:871
  • PLBY Lean proofsErdosProblems.Erdos871

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI building on literature

    Erdős AI contributions wiki · 5 Jan, 2026

    Machine
    Claude Opus 4.5, Gemini 3 Pro
    Open the source record

  • construction

    VibeMathed

    Machine
    Claude Opus 4.5, Gemini 3 Pro
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page