Skip to content

Erdős problem 38

Start work

Does there exist B⊂NB \subset \mathbb{N} which is not an additive basis, but is such that for every set A⊆NA \subseteq \mathbb{N} of Schnirelmann density α\alpha and every NN there exists b∈Bb \in B such that ∣(A∪(A+b))∩{1,…,N}∣≥(α+f(α))N \lvert (A \cup (A+b)) \cap \{1, \ldots, N\} \rvert \geq (\alpha + f(\alpha)) N where f(α)>0f(\alpha) > 0 for 0<α<10 < \alpha < 1?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/38.lean

Formal Conjectures

FormalConjectures/ErdosProblems/38.leanErdos38.erdos_388 linesExact file
True ↔  ∃ B,    ¬B.IsWeakAddBasis ∧      ∃ f,        (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧          ∀ (A : Set ℕ) (N : ℕ),            have α := schnirelmannDensity A;            ∃ b ∈ B, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑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:38
  • PLBY Lean proofsErdosProblems.Erdos38

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry