Formal target: Corpus.OEIS67857.conjecture

The terms are not all positive.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    Iff (LT.lt.{0} (Corpus.OEIS67857.a n) 0)
      (And (Odd.{0} (DFunLike.coe.{1, 1, 1} ArithmeticFunction.cardDistinctFactors n))
        (LE.le.{0} 3 (DFunLike.coe.{1, 1, 1} ArithmeticFunction.cardDistinctFactors n)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record