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 1i<jτ(n)1djdi1+1i<τ(n)1di+1di\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 nn \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)?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/884.lean

Formal Conjectures

FormalConjectures/ErdosProblems/884.leanErdos884.erdos_8841 lineExact file
FalseErdos884.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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:884

Continue

Search problems.science

Find a Problem, Result, source, or page