Erdős problem 298 · problems.science

Does every set $A \subseteq \mathbb{N}$ of positive density contain some finite $S \subset A$ such that $\sum_{n \in S} \frac{1}{n} = 1$ ?

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

298.lean

Retained formal statement1 of 2

Does every set $A \subseteq \mathbb{N}$ of positive density contain some finite $S \subset A$ such that $\sum_{n \in S} \frac{1}{n} = 1$ ?

The answer is yes, proved by Bloom [Bl21] (even if 'positive density' is interpreted as 'positive upper density', which is likely what Erdős intended).

The theorem below uses the positive-upper-density interpretation; the literal natural-density interpretation is recorded separately.

This was formalized in Lean 3 by Bloom and Mehta.

FormalConjectures/ErdosProblems/298.leanErdos298.erdos_2981 lineExact file

1True ↔ ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity → ∃ S, ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

SolvedProof has a holeother systemexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science