Formal target: Corpus.Erdos889.erdos_889
Let $v(n,k)$ count the prime factors of $n+k$ which do not divide $n+i$ for $0\leq i < k$.
Exact formal statement
Filter.Tendsto.{0, 0} Corpus.Erdos889.v₀ Filter.atTop.{0} (nhds.{0} Top.top.{0})This target is a formal statement, not a proof of the problem.
Environment availability: available.