1. FormalConjectures
  2. ErdosProblems
  3. «884»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil import FormalConjectures.Wikipedia.HardyLittlewood

Erdős Problem 884

References:

namespace Erdos884

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$.

noncomputable abbrev sumDivisorInvPairwiseDifference (n : ℕ) : ℝ := ∑ j : Fin n.divisors.card, ∑ i : Fin j, (1 : ℚ) / (Nat.nth (· ∣ n) j - Nat.nth (· ∣ n) i )

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

noncomputable abbrev sumDivisorInvConsecutiveDifference (n : ℕ) : ℝ := ∑ i : Fin (n.divisors.card - 1), (1 : ℚ) / (Nat.nth (· ∣ n) (i + 1) - Nat.nth (· ∣ n) i)

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.

def Erdos884Prop : Prop := sumDivisorInvPairwiseDifference ≪ 1 + sumDivisorInvConsecutiveDifference

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

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_884 : answer(False) ↔ Erdos884Prop := ⊢ False ↔ Erdos884Prop All goals completed! 🐙

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.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_884_false_of_hardy_littlewood : ∀ (k : ℕ) (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m → ¬Erdos884Prop := ⊢ ∀ (k : ℕ) (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m → ¬Erdos884Prop All goals completed! 🐙 end Erdos884