Formal target: Corpus.OEIS1223.conjecture

Any subsequence a(n ..

Exact formal statement

∀ (n m : Nat),
  GE.ge.{0} n 3 →
    Set.Infinite.{0}
      (Set.ofPred.{0} fun k =>
        Eq.{1} (Corpus.OEIS1223.gapSubsequence k (HAdd.hAdd.{0, 0, 0} m 1))
          (Corpus.OEIS1223.gapSubsequence n (HAdd.hAdd.{0, 0, 0} m 1)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record