Formal target: Corpus.Erdos1095.erdos_1095.variants.upper_conjecture

Ecklund, Erdős, and Selfridge [EES74] conjectured $g(k)\leq \exp((1+o(1))k)$.

Exact formal statement

Exists.{1} fun f =>
  And (Filter.Tendsto.{0, 0} f Filter.atTop.{0} (nhds.{0} 0))
    (Filter.Eventually.{0}
      (fun k =>
        LE.le.{0} (Nat.cast.{0} (Corpus.Erdos1095.g k))
          (Real.exp (HMul.hMul.{0, 0, 0} (Nat.cast.{0} k) (HAdd.hAdd.{0, 0, 0} 1 (f k)))))
      Filter.atTop.{0})

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record