Skip to content

Erdős problem 290

Let a1a\geq 1. Must there exist some b>ab>a such that anb1n=r1s1 and anb+11n=r2s2,\sum_{a\leq n\leq b}\frac{1}{n}=\frac{r_1}{s_1}\textrm{ and } \sum_{a\leq n\leq b+1}\frac{1}{n}=\frac{r_2}{s_2}, with (ri,si)=1(r_i,s_i)=1 and s2<s1s_2<s_1? If so, how does this b(a)b(a) grow with aa?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

290.lean

Retained formal statement1 of 1

Let a1a\geq 1. Must there exist some b>ab>a such that anb1n=r1s1 and anb+11n=r2s2,\sum_{a\leq n\leq b}\frac{1}{n}=\frac{r_1}{s_1}\textrm{ and } \sum_{a\leq n\leq b+1}\frac{1}{n}=\frac{r_2}{s_2}, with (ri,si)=1(r_i,s_i)=1 and s2<s1s_2<s_1? If so, how does this b(a)b(a) grow with aa?

This was resolved in the affirmative by van Doorn [vD24], who proved b=b(a)b=b(a) always exists, and in fact b(a)ab(a) \ll a. Indeed, if a(3k,3k+1]a\in (3^k,3^{k+1}] then one can take b=23k+11b=2\cdot 3^{k+1}-1. van Doorn also proves that b(a)>a+(1/2o(1))logab(a)>a+(1/2-o(1))\log a, and considers various generalisations of the original problem.

FormalConjectures/ErdosProblems/290.leanErdos290.erdos_2901 lineExact file
True ↔ ∀ (a : ℕ), 1 ≤ a → ∃ b, a < bErdos290.harmonicDen a (b + 1) < Erdos290.harmonicDen a b
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