Conjectures.io

Number theory

Erdős 889

Let v(n,k)v(n,k) count the prime factors of n+kn+k which do not divide n+in+i for 0≤i<k0\leq i < k. Is it true that v0(n)=max⁡k≥0v(n,k)→∞v_0(n)=\max_{k\geq 0}v(n,k)\to \infty as n→∞n\to \infty?

References

No one has attempted this yet.

Formal statement

Lean type

Filter.Tendsto Erdos889.v₀ Filter.atTop (nhds ⊤)

What you must prove

import FormalConjectures.ErdosProblems.«889»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos889.erdos_889" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/889.lean

Source type SHA-256
sha256:f226cfb184f5af0bae007b9b98986ae3cbfa840c57e651080c93214f44e01a58
Task id
fc-379fc029-erdos889-erdos-889-081cbb5cd6-formalized-v1
Task commitment
sha256:f36fcb1b936ab188f8c80b6d75e8311dac6c664670577d8335b00940269ab272

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.