Erdős problem 208

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

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