Skip to content

Erdős problem 316

Is it true that if A⊆N∖{1}A \subseteq \mathbb{N}\setminus\{1\} is a finite set with ∑n∈A1n<2\sum_{n \in A} \frac{1}{n} < 2 then there is a partition A=A1⊔A2A=A_1 \sqcup A_2 such that ∑n∈Ai1n<1\sum_{n \in A_i} \frac{1}{n} < 1 for i=1,2i=1,2?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

316.lean

Retained formal statement2 of 3

This is not true in general, as shown by Sándor [Sa97], who observed that the proper divisors of 120120 form a counterexample. More generally, Sándor shows that for any n≥2n\geq 2 there exists a finite set A⊆N\{1}A\subseteq \mathbb{N}\backslash\{1\} with ∑k∈A1k<n\sum_{k\in A}\frac{1}{k} < n and no partition into nn parts each of which has ∑k∈Ai1k<1\sum_{k\in A_i}\frac{1}{k}<1.

FormalConjectures/ErdosProblems/316.leanErdos316.erdos_316.variants.generalized6 linesExact file
∀ (n : ℕ),  2 ≤ n →    ∃ A,      A.Nonempty ∧        0 ∉ A ∧          1 ∉ A ∧ ∑ k ∈ A, 1 / ↑k < ↑n ∧ ∀ (P : Finpartition A), P.parts.card = n → ∃ p ∈ P.parts, 1 ≤ ∑ n ∈ p, 1 / ↑n
SolvedStatement only, no proof