Number theory

Erdős 208 - log bound

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.

References

erdosproblems.com/208

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«208»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos208.erdos_208.variants.log_bound" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/208.lean

Source type SHA-256: sha256:f934595c12d4ec6e259b6f51b8f416436bdd092e9e2ce1d85daaa0c54f295023
Task id: fc-379fc029-variants-log-bound-f4b3b30352-formalized-v1
Task commitment: sha256:00bbacaa394f8d7b0a23e2ab65a879bed141763335e7fcc35badd876913b90f5

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.