Formal target: Corpus.OEIS167918.conjecture1

Conjecture: $f(n, k) = 2$ for infinitely many cases, where $k = a(n)$.

Exact formal statement

∀ (M : Nat),
  (∀ (n : Nat), GT.gt.{0} n 0 → Ne.{1} (Corpus.OEIS167918.a n) 0) →
    Exists.{1} fun n =>
      And (GE.ge.{0} n M)
        (And (GT.gt.{0} n 0)
          (Eq.{1} (Corpus.OEIS167918.S (Corpus.OEIS167918.a n)) (HMul.hMul.{0, 0, 0} 2 (Corpus.OEIS167918.S n))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record