Skip to content

Erdős problem 337

Let A⊆NA\subseteq \mathbb{N} be an additive basis (of any finite order) such that ∣A∩{1,…,N}∣=o(N)\lvert A\cap \{1,\ldots,N\}\rvert=o(N). Is it true that lim⁡N→∞∣(A+A)∩{1,…,N}∣∣A∩{1,…,N}∣=∞? \lim_{N\to \infty}\frac{\lvert (A+A)\cap \{1,\ldots,N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/337.lean

Formal Conjectures

FormalConjectures/ErdosProblems/337.leanErdos337.erdos_3375 linesExact file
False ↔  ∀ (A : Set ℕ),    A.IsAsymptoticAddBasis →      ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) →        Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTop
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:337
  • PLBY Lean proofsErdosProblems.Erdos337

Reported activity

Reported by these sources. Not reviewed here.

Continue