Skip to content

Erdős problem 170

Start work

The problem is to determine the limit of the sequence F(N)N\frac{F(N)}{\sqrt{N}} as N→∞N \to \infty.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

170.lean

Retained formal statement2 of 3

The existence of the limit has been proved by Erdős and Gál [ErGa48]. The lower bound has been proven by Leech [Le56], who refined an argument of Rédei and Rényi. The upper bound is due to Wichmann [Wi63].

FormalConjectures/ErdosProblems/170.leanErdos170.erdos170.existing_bounds2 linesExact file
∃ x ∈ Set.Icc Erdos170.lower_bound Erdos170.upper_bound,  Filter.Tendsto (fun N => ↑(Erdos170.F N) / √↑N) Filter.atTop (nhds x)
SolvedStatement only, no proof