Formal target: Corpus.OEIS72200.conjecture

It is conjectured that $a(24) = 0$ since no factorial less than $10000$ contained just 24 sixes.

Exact formal statement

Eq.{1} (Corpus.OEIS72200.a 24) 0

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

Environment availability: available.