Erdős problem 170 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

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

1∃ x ∈ Set.Icc Erdos170.lower_bound Erdos170.upper_bound,2  Filter.Tendsto (fun N => ↑(Erdos170.F N) / √↑N) Filter.atTop (nhds x)

SolvedStatement only, no proof

Sources

Search problems.science