Erdős Problem 885

References:

• erdosproblems.com/885
• [ErRo97] Erdős, P. and Rosenfeld, M., The factor-difference set of integers. (1997)
• [Ji99] Jiménez-Urroz, J., A note on a conjecture of Erdős and {R}osenfeld. (1999)
• [Br19] Bremner, A., On a problem of Erdős related to common factor differences. (2019)

def Erdos885.factorDifferenceSet (n : ℕ) : Set ℕ

For integer $n \geq 1$ we define the factor difference set of $n$ by $D(n) = \{|a-b| : n=ab\}$.

Equations

• Erdos885.factorDifferenceSet n = {d : ℕ | ∃ (a : ℕ) (b : ℕ), n = a * b ∧ ↑d = |↑a - ↑b|}

theorem Erdos885.erdos_885 : sorry ↔ ∀ k ≥ 1, ∃ (Ns : Finset ℕ), (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = k ∧ (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ k

Is it true that, for every $k \geq 1$, there exist integers $N_1 < \dots < N_k$ such that $|\cap_i D(N_i)| \geq k$?

theorem Erdos885.erdos_885.variants.k_eq_2 : ∃ (Ns : Finset ℕ), (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = 2 ∧ (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 2

Erdős and Rosenfeld [ErRo97] proved this is true for $k=2$.

theorem Erdos885.erdos_885.variants.k_eq_3 : ∃ (Ns : Finset ℕ), (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = 3 ∧ (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 3

Jiménez-Urroz [Ji99] proved this for $k=3$.

theorem Erdos885.erdos_885.variants.k_eq_4 : ∃ (Ns : Finset ℕ), (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = 4 ∧ (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 4

Bremner [Br19] proved this for $k=4$.