Formal target: Corpus.OEIS117027.conjecture

This suggests the ratio is approaching a limit close to 0.87.

Exact formal statement

Exists.{1} fun L =>
  And (Filter.Tendsto.{0, 0} Corpus.OEIS117027.ratioSeq Filter.atTop.{0} (nhds.{0} L))
    (And (LT.lt.{0} 0.8 L) (LT.lt.{0} L 0.9))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record