Erdős problem 208 · problems.science

In [Er79] Erdős says perhaps $s_{n+1} - s_n \ll \log s_n$ , but he is 'very doubtful'.

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

208.lean

Retained formal statement3 of 3

In [Er79] Erdős says perhaps $s_{n+1} - s_n \ll \log s_n$ , but he is 'very doubtful'.

[Er79] Erdős, Paul, __Some unconventional problems in number theory__. Math. Mag. (1979), 67-70.

FormalConjectures/ErdosProblems/208.leanErdos208.erdos_208.variants.log_bound2 linesExact file

1(fun n => ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n)) =O[Filter.atTop] fun n =>2  Real.log ↑(Erdos208.erdos208.s n)

OpenStatement only, no proof