Erdős problem 884 · problems.science

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$ )?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

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](https://terrytao.wordpress.com/wp-content/uploads/2025/09/erdos-884.pdf). 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

1∀ (k : ℕ) (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m → ¬Erdos884.Erdos884Prop

SolvedStatement only, no proof

Sources

Search problems.science