Erdős Problem 884

References:

• erdosproblems.com/884
• Tao25
• Larsen

@[reducible, inline]

noncomputable abbrev Erdos884.sumDivisorInvPairwiseDifference (n : ℕ) : ℝ

The sum $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i}$ over all pairs of divisors $d_i < d_j$ of $n$.

Equations

• Erdos884.sumDivisorInvPairwiseDifference n = ∑ j : Fin n.divisors.card, ∑ i : Fin ↑j, ↑1 / (↑(Nat.nth (fun (x : ℕ) => x ∣ n) ↑j) - ↑(Nat.nth (fun (x : ℕ) => x ∣ n) ↑i))

@[reducible, inline]

noncomputable abbrev Erdos884.sumDivisorInvConsecutiveDifference (n : ℕ) : ℝ

The sum $\sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}$ over consecutive divisors of $n$.

Equations

• Erdos884.sumDivisorInvConsecutiveDifference n = ∑ i : Fin (n.divisors.card - 1), ↑1 / (↑(Nat.nth (fun (x : ℕ) => x ∣ n) (↑i + 1)) - ↑(Nat.nth (fun (x : ℕ) => x ∣ n) ↑i))

def Erdos884.Erdos884Prop : Prop

For a natural number n, let $1 = d_1 < \dotsc < d_{\tau(n)} = n$ denote the divisors of $n$ in increasing order. Does it hold that $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \ll 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}$ for $n \to \infty`, i.e. $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \in O \left( 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}) \right)$?

This conjecture has been disproved:

• In September 2025, Terence Tao gave a conditional negative answer assuming the prime tuples conjecture, see erdos_884_false_of_hardy_littlewood for this implication.
• Daniel Larsen subsequently gave an unconditional disproof.

Equations

• Erdos884.Erdos884Prop = Erdos884.sumDivisorInvPairwiseDifference =O[Filter.atTop] (1 + Erdos884.sumDivisorInvConsecutiveDifference)

theorem Erdos884.erdos_884 : False ↔ Erdos884Prop

For a natural number n, let $1 = d_1 < \dotsc < d_{\tau(n)} = n$ denote the divisors of $n$ in increasing order. Does it hold that $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \ll 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}$ for $n \to \infty`, i.e. $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \in O \left( 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}) \right)$?

This conjecture has been disproved:

• In September 2025, Terence Tao gave a conditional negative answer assuming the prime tuples conjecture, see erdos_884_false_of_hardy_littlewood for this implication.
• Daniel Larsen subsequently gave an unconditional disproof.

Reference: erdosproblems.com/884

theorem Erdos884.erdos_884_false_of_hardy_littlewood (k : ℕ) (m : Fin k.succ → ℕ) : HardyLittlewood.FirstHardyLittlewoodConjectureFor m → ¬Erdos884Prop

In September 2025, Terence Tao gave a conditional negative answer to Erdos conjecture 884, disproving it under the assumption of the Qualitative Hardy-Littlewood Conjecture. See here. The qualitative version of the conjecture only states that there are infinitely many tuples of primes and does not require any asymptotical bounds and as such is a corollary of the general form of the Hardy-Littlewood Conjecture. We state the 'weaker' implication using general Hardy-Littlewood here, since this conjecture is already formalized.