FormalConjectures/ErdosProblems/884.lean

GitHub source file

5 declarations, 2 contain sorry, 0 declared as axioms

1. abbrev Erdos884.sumDivisorInvPairwiseDifference 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$ line 37 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real

   Proof uses: Finset.sum, Fin, Finset.card, Nat.divisors, Finset.univ, HDiv.hDiv, OfNat.ofNat, Rat, HSub.hSub, Nat.nth, Dvd.dvd

   14 instances, coercions and auxiliary constants left out.

   noncomputable abbrev sumDivisorInvPairwiseDifference (n : ℕ) : ℝ :=
   …

2. abbrev Erdos884.sumDivisorInvConsecutiveDifference The sum $\sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}$ over consecutive divisors of $n$ line 45 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real

   Proof uses: Finset.sum, Fin, HSub.hSub, Finset.card, Nat.divisors, OfNat.ofNat, Finset.univ, HDiv.hDiv, Rat, Nat.nth, Dvd.dvd, HAdd.hAdd

   18 instances, coercions and auxiliary constants left out.

   noncomputable abbrev sumDivisorInvConsecutiveDifference (n : ℕ) : ℝ :=
   …

3. def Erdos884.Erdos884Prop For a natural number n, let $1 = d_1 < \dotsc < d_{\tau(n)} = n$ denote the divisors of $n$ in increasing order line 64 source

   Source documentation

   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.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Proof uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos884.sumDivisorInvPairwiseDifference, HAdd.hAdd, OfNat.ofNat, Erdos884.sumDivisorInvConsecutiveDifference

   8 instances, coercions and auxiliary constants left out.

   def Erdos884Prop : Prop :=
   …

4. theorem Erdos884.erdos_884 For a natural number n, let $1 = d_1 < \dotsc < d_{\tau(n)} = n$ denote the divisors of $n$ in increasing order sorry line 86 source

   Source documentation

   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

   L4DEL explanation

   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

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, False, Erdos884.Erdos884Prop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_884 :
       answer(False) ↔ Erdos884Prop := by
   …

   Mentions: Erdos884.Erdos884Prop

5. theorem Erdos884.erdos_884_false_of_hardy_littlewood Documented declaration: erdos_884_false_of_hardy_littlewood sorry line 103 source

   Source documentation

   In September 2025, Terence Tao gave a conditional negative answer to Erdős problem 884, disproving it under the assumption of the qualitative Hardy–Littlewood prime tuples conjecture, see Conjecture 1.1 and Theorem 1.1 of Tao25.

   The qualitative conjecture states that for every admissible tuple $(h_1, \dotsc, h_k)$ of integers, i.e. one which avoids at least one residue class modulo $p$ for every prime $p$, there are infinitely many natural numbers $n$ such that $n + h_1, \dotsc, n + h_k$ are all prime. Unlike the full Hardy–Littlewood conjecture, it does not give an asymptotic for the number of such $n$.

   L4DEL explanation

   In September 2025, Terence Tao gave a conditional negative answer to Erdős problem 884, disproving it under the assumption of the qualitative Hardy–Littlewood prime tuples conjecture, see Conjecture 1.1 and Theorem 1.1 of Tao25. The qualitative conjecture states that for every admissible tuple $(h_1, \dotsc, h_k)$ of integers, i.e. one which avoids at least one residue class modulo $p$ for every prime $p$, there are infinitely many natural numbers $n$ such that $n + h_1, \dotsc, n + h_k$ are all prime. Unlike the full Hardy–Littlewood conjecture, it does not give an asymptotic for the number of such $n$.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Finset, Int, Nat, Nat.Prime, Exists, Membership.mem, Not, Dvd.dvd, HAdd.hAdd, Set.Infinite, Set.ofPred, Prime, Erdos884.Erdos884Prop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   19 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_884_false_of_hardy_littlewood
       (hHL : ∀ H : Finset ℤ, (∀ p : ℕ, p.Prime → ∃ a : ℤ, ∀ h ∈ H, ¬ (p : ℤ) ∣ a + h) →
         {n : ℕ | ∀ h ∈ H, Prime ((n : ℤ) + h)}.Infinite) :
       ¬Erdos884Prop := by
   …

   Mentions: Erdos884.Erdos884Prop