Formal target: Corpus.OEIS105020.conjecture

A "Goldbach Conjecture" for this sequence: when there are $n$ terms between consecutive odd integers $2n+1$ and $2n+3$ for $n > 0$, at least one will be the product of 2 primes (not necessarily distinct).

Exact formal statement

∀ (n i j : Nat),
  LE.le.{0} 1 n →
    Eq.{1} (Corpus.OEIS105020.a i) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 n) 1) →
      Eq.{1} (Corpus.OEIS105020.a j) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 n) 3) →
        Eq.{1} j (HAdd.hAdd.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} i n) 1) →
          Exists.{1} fun k => And (LT.lt.{0} i k) (And (LT.lt.{0} k j) (Corpus.OEIS105020.a k).IsSemiprime)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record