Skip to content

Erdős problem 314

Let n≥1n\geq 1 and let mm be minimal such that ∑n≤k≤m1k≥1\sum_{n\leq k\leq m}\frac{1}{k}\geq 1. We define ϵ(n)=∑n≤k≤m1k−1.\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1. How small can ϵ(n)\epsilon(n) be? Is it true that lim inf⁡n2ϵ(n)=0?\liminf n^2\epsilon(n)=0?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/314.lean

Formal Conjectures

FormalConjectures/ErdosProblems/314.leanErdos314.erdos_3141 lineExact file
True ↔ Filter.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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:314
  • PLBY Lean proofsErdosProblems.Erdos314

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page