Formal target: Corpus.OEIS145355.conjecture

This sequence suggests that the distance between a factorial and the closest power is tightly bounded.

Exact formal statement

Exists.{1} fun C => ∀ (n : Nat), LE.le.{0} 2 n → LE.le.{0} (Corpus.OEIS145355.a n) C

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

Environment availability: available.