Formal target: Corpus.OEIS93456.conjecture

Conjecture: There are finitely many numbers such that $a(n)$ is not $\equiv 0 \pmod{a(n-1)}$.

Exact formal statement

Set.Finite.{0}
  (Set.ofPred.{0} fun n =>
    And (LT.lt.{0} 1 n) (Not (Dvd.dvd.{0} (Corpus.OEIS93456.a (HSub.hSub.{0, 0, 0} n 1)) (Corpus.OEIS93456.a n))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record