Erdős problem 316 · problems.science

Is it true that if $A \subseteq \mathbb{N}\setminus\{1\}$ is a finite set with $\sum_{n \in A} \frac{1}{n} < 2$ then there is a partition $A=A_1 \sqcup A_2$ such that $\sum_{n \in A_i} \frac{1}{n} < 1$ for $i=1,2$ ?

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

316.lean

Retained formal statement3 of 3

This is not true if $A$ is a multiset, for example $2,3,3,5,5,5,5$ .

FormalConjectures/ErdosProblems/316.leanErdos316.erdos_316.variants.multiset17 linesExact file

1∃ A,2  0 ∉ A ∧3    1 ∉ A ∧4      (Multiset.map (fun x => 1 / x) do5              let a ← A6              pure ↑a).sum <7          2 ∧8        ∀ (A₁ A₂ : Multiset ℕ),9          A = A₁ + A₂ →10            1 ≤11                (Multiset.map (fun x => 1 / x) do12                    let a ← A₁13                    pure ↑a).sum ∨14              1 ≤15                (Multiset.map (fun x => 1 / x) do16                    let a ← A₂17                    pure ↑a).sum

TextbookStatement only, no proof

Sources

Search problems.science