Erdős problem 33

Let `A ⊆ ℕ` be a set such that every integer can be written as `n^2 + a` for some `a` in `A` and `n ≥ 0`. What is the smallest possible value of `lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2)`?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

33.lean

Retained formal statement2 of 3

Erdos observed that this value is finite and > 1.

FormalConjectures/ErdosProblems/33.leanErdos33.erdos_33.variants.one_mem_lowerBounds1 lineExact file

1∃ A, Erdos33.AdditiveBasisCondition A ∧ 1 < Filter.limsup (fun N => ↑(A ∩ Set.Icc 1 N).ncard / √↑N) Filter.atTop

SolvedStatement only, no proof