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
FormalConjectures/ErdosProblems/
33.lean
Retained formal statement
The smallest possible value of lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) is at most 2φ^(5/2) ≈ 6.66, with φ equal to the golden ratio. Proven by Wouter van Doorn.
⨅ A, Filter.limsup (fun N => ↑(↑A ∩ Set.Icc 1 N).ncard / ↑√↑N) Filter.atTop ≤ ↑(2 * Real.goldenRatio ^ (5 / 2))SolvedStatement only, no proof