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 ∑a∈A1a>δlog⁡N\sum_{a\in A}\frac{1}{a}>\delta \log N then must there exist S⊆AS\subseteq A such that ∑n∈S1n=1\sum_{n\in S}\frac{1}{n}=1?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

47.lean

Retained formal statement1 of 1

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 ∑a∈A1a>δlog⁡N\sum_{a\in A}\frac{1}{a}>\delta \log N then must there exist S⊆AS\subseteq A such that ∑n∈S1n=1\sum_{n\in S}\frac{1}{n}=1?

Bloom [Bl21] proved this in the affirmative.

FormalConjectures/ErdosProblems/47.leanErdos47.erdos_474 linesExact file
True ↔  ∀ (δ : ℝ),    0 < δ →      ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, δ * Real.log ↑N < A.reciprocalSum → ∃ S ⊆ A, 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.

Search problems.science

Find a Problem, Result, source, or page