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

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

316.lean

Retained formal statement1 of 3

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?

This is not true in general, as shown by Sándor [Sa97].

The minimal counterexample is {2,3,4,5,6,7,10,11,13,14,15}\{2,3,4,5,6,7,10,11,13,14,15\}, found by Tom Stobart.

This was formalized in Lean by Mehta.

FormalConjectures/ErdosProblems/316.leanErdos316.erdos_3164 linesExact file
False ↔  ∀ (A : Finset ℕ),    0 ∉ A →      1 ∉ A → ∑ n ∈ A, 1 / ↑n < 2 → ∃ A₁ A₂, Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧ ∑ n ∈ A₁, 1 / ↑n < 1 ∧ ∑ n ∈ A₂, 1 / ↑n < 1
SolvedProved, no gapslean4external proof

Search problems.science

Find a Problem, Result, source, or page