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$ ?

No current result

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

FormalConjectures/ErdosProblems/298.lean

Formal Conjectures

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.