Erdős problem 47

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

47.lean

Retained formal statement1 of 1

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

Bloom [Bl21] proved this in the affirmative.

FormalConjectures/ErdosProblems/47.leanErdos47.erdos_474 linesExact file

1True ↔2  ∀ (δ : ℝ),3    0 < δ →4      ∀ᶠ (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.