Skip to content

Erdős problem 208

In [Er79] Erdős says perhaps sn+1−sn≪log⁡sns_{n+1} - s_n \ll \log s_n, but he is 'very doubtful'.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/208.lean

Formal Conjectures

FormalConjectures/ErdosProblems/208.leanErdos208.erdos_208.parts.i4 linesExact file
True ↔  ∀ ε > 0,    (fun n => ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n)) =O[Filter.atTop] fun n =>      ↑(Erdos208.erdos208.s n) ^ ε
OpenStatement only, no proof

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page