Formal target: Corpus.OEIS182126.conjecture1

Conjecture: For $x > 10^9$, the most frequent value in $a(n)$, $n=1\dots x$, has form $120k$.

Exact formal statement

∀ (x : Nat),
  LT.lt.{0} (HPow.hPow.{0, 0, 0} 10 9) x → ∀ (v₀ : Nat), Corpus.OEIS182126.IsMostFrequent x v₀ → Dvd.dvd.{0} 120 v₀

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

Environment availability: available.