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 statement2 of 2

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.

FormalConjectures/ErdosProblems/884.leanErdos884.erdos_884_false_of_hardy_littlewood1 lineExact file
∀ (k : ℕ) (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m → ¬Erdos884.Erdos884Prop
SolvedStatement only, no proof