Skip to content

Erdős problem 884

For a natural number n, let 1=d1<…<dτ(n)=n1 = d_1 < \dotsc < d_{\tau(n)} = n denote the divisors of n in increasing order. Does it hold that ∑1≤i<j≤τ(n)1dj−di≪1+∑1≤i<τ(n)1di+1−di\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→∞‘n \to \infty`, i.e. Unparsed notation: \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}) Unparsed notation: \right)?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

884.lean

Retained formal statement1 of 2

For a natural number n, let 1=d1<…<dτ(n)=n1 = d_1 < \dotsc < d_{\tau(n)} = n denote the divisors of n in increasing order. Does it hold that ∑1≤i<j≤τ(n)1dj−di≪1+∑1≤i<τ(n)1di+1−di\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→∞‘n \to \infty`, i.e. Unparsed notation: \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}) Unparsed notation: \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

FormalConjectures/ErdosProblems/884.leanErdos884.erdos_8841 lineExact file
False ↔ Erdos884.Erdos884Prop
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.