Formal target: Corpus.OEIS157237.conjecture
On Feb.
Exact formal statement
∀ (n : Nat),
LT.lt.{0} 0 n →
Iff (Eq.{1} (Corpus.OEIS157237.a n) 0)
(Or (LE.le.{0} n 15)
(Or (Eq.{1} n 18)
(Or (Eq.{1} n 21)
(Or (Eq.{1} n 24) (Or (Eq.{1} n 51) (Or (Eq.{1} n 84) (Or (Eq.{1} n 1011) (Eq.{1} n 59586))))))))This target is a formal statement, not a proof of the problem.
Environment availability: available.