Skip to content

Erdős problem 47

If δ>0\delta>0 and NN is sufficiently large in terms of δ\delta, and A{1,,N}A\subseteq\{1,\ldots,N\} is such that aA1a>δlogN\sum_{a\in A}\frac{1}{a}>\delta \log N then must there exist SAS\subseteq A such that nS1n=1\sum_{n\in S}\frac{1}{n}=1?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/47.lean

Formal Conjectures

FormalConjectures/ErdosProblems/47.leanErdos47.erdos_474 linesExact file
True  ∀ (δ : ℝ),    0 < δ →      ∀ᶠ (N : ℕ) in Filter.atTop, ∀ AFinset.Icc 1 N, δ * Real.logN < A.reciprocalSum → ∃ SA, S.reciprocalSum = 1
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:47
  • PLBY Lean proofsErdosProblems.Erdos47

Continue

Search problems.science

Find a Problem, Result, source, or page