Skip to content

Erdős problem 881

Start work

Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

881.lean

Retained formal statement1 of 1

Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.

Must there exist an infinite B ⊂ A such that A \ B is an additive basis of order k + 1?

FormalConjectures/ErdosProblems/881.leanErdos881.erdos_8813 linesExact file
True ↔  ∀ (k : ℕ) (A : Set ℕ),    Erdos881.IsMinimalAsymptoticAddBasisOfOrder k A → ∃ B ⊆ A, B.Infinite ∧ (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)
OpenStatement only, no proof