Skip to content

Erdős problem 314

Let n1n\geq 1 and let mm be minimal such that nkm1k1\sum_{n\leq k\leq m}\frac{1}{k}\geq 1. We define ϵ(n)=nkm1k1.\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1. How small can ϵ(n)\epsilon(n) be? Is it true that lim infn2ϵ(n)=0?\liminf n^2\epsilon(n)=0?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

314.lean

Retained formal statement1 of 1

Let n1n\geq 1 and let mm be minimal such that nkm1k1\sum_{n\leq k\leq m}\frac{1}{k}\geq 1. We define ϵ(n)=nkm1k1.\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1. How small can ϵ(n)\epsilon(n) be? Is it true that lim infn2ϵ(n)=0?\liminf n^2\epsilon(n)=0?

This is true, and shown by Lim and Steinerberger [LiSt24], who further proved that, for any δ>0\delta>0, there exist infinitely many nn and mm such that n2nkm1k11(logn)5/4δ.n^2\left\lvert \sum_{n\leq k\leq m}\frac{1}{k}-1\right\rvert\ll \frac{1}{(\log n)^{5/4-\delta}}. Erdős and Graham (and also Lim and Steinerberger) believe that the exponent of 22 is best possible here, in that lim infϵ(n)n2+δ=\liminf \epsilon(n) n^{2+\delta}=\infty for all δ>0\delta>0.

FormalConjectures/ErdosProblems/314.leanErdos314.erdos_3141 lineExact file
TrueFilter.liminf (fun n => ↑n ^ 2 * Erdos314.epsilon n) Filter.atTop = 0
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.

Search problems.science

Find a Problem, Result, source, or page