Number theory · Last catalog review 26 Jul 2026

Erdős Problem 889

Let

v(n,k)

count the prime factors of

n+k

which do not divide

n+i

for

0\leq i < k

. Is it true that

v_0(n)=\max_{k\geq 0}v(n,k)\to \infty

n\to \infty

References

erdosproblems.com/889

Published 27 Jul 2026Never attempted

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-e923379e-erdos889-erdos-889-67b2dac080-formalized-v1
Task commitment: sha256:930f751e1cb383c252ba23e76f36d63433f7e17c05604a407102d4a5713cd700

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.