Skip to content

Erdős problem 290

Start work

Let a≥1a\geq 1. Must there exist some b>ab>a such that ∑a≤n≤b1n=r1s1 and ∑a≤n≤b+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?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/290.lean

Formal Conjectures

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

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:290
  • PLBY Lean proofsErdosProblems.Erdos290

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry