Erdős Problem 889

Reference: erdosproblems.com/889

def Erdos889.v (n k : ℕ) : ℕ

$v(n,k)$ counts the prime factors of $n+k$ which do not divide $n+i$ for all $0 \le i < k$.

Equations

• Erdos889.v n k = {p ∈ (n + k).primeFactors | ∀ i ∈ Finset.range k, ¬p ∣ n + i}.card

noncomputable def Erdos889.v₀ (n : ℕ) : ℕ∞

$v_0(n)$ is the supremum of $v(n,k)$ for all $k \ge 0$.

Equations

• Erdos889.v₀ n = ⨆ (k : ℕ), ↑(Erdos889.v n k)

theorem Erdos889.erdos_889 : Filter.Tendsto v₀ Filter.atTop (nhds ⊤)

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$ as $n\to \infty$?

theorem Erdos889.erdos_889.variants.v0_gt_1 (n : ℕ) : n ∉ {0, 1, 2, 3, 4, 7, 8, 16} → 1 < v₀ n

$v_0(n) > 1$ for all $n$ except $n$ = 0, 1, 2, 3, 4, 7, 8, 16

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

noncomputable def Erdos889.v_l (l n : ℕ) : ℕ∞

$v_l(n)$ is the supremum of $v(n,k)$ for all $k \ge l$

Equations

• Erdos889.v_l l n = ⨆ (k : ℕ), ⨆ (_ : k ≥ l), ↑(Erdos889.v n k)

theorem Erdos889.erdos_889.variants.general (l : ℕ) : Filter.Tendsto (v_l l) Filter.atTop (nhds ⊤)

Let $v_l(n) = \max_{k\geq l} v(n,k)$. For every fixed $l$, $v_l(n) \to \infty$ as $n \to \infty$

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

theorem Erdos889.erdos_889.variants.v1_eq_1_finite : {n : ℕ | v_l 1 n = 1}.Finite ↔ sorry

Does $v_1(n) = 1$ have finite solutions?

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

def Erdos889.V (n k : ℕ) : ℕ

$V(n,k)$ is the number of primes $p$ such that $p^\alpha$ exactly divides $n+k$ and for all $0 \le i < k$, $p^\alpha$ does not divide $n+i$, where $\alpha$ is the multiplicity of $p$ in the factorization of $n+k$.

Equations

• Erdos889.V n k = {p ∈ (n + k).primeFactors | ∀ i ∈ Finset.range k, ¬p ^ (n + k).factorization p ∣ n + i}.card

noncomputable def Erdos889.V_l (l n : ℕ) : ℕ∞

$V_l(n)$ is the supremum of $V(n,k)$ for all $k \ge l$

Equations

• Erdos889.V_l l n = ⨆ (k : ℕ), ⨆ (_ : k ≥ l), ↑(Erdos889.V n k)

theorem Erdos889.erdos_889.variants.V1_eq_1_finite : {n : ℕ | V_l 1 n = 1}.Finite ↔ sorry

Does $V_1(n) = 1$ have finite solutions?

This is a modification of erdos_889.variants.v1_eq_1_finite, which might make it more amenable to attack according to [ErSe67].

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.