Skip to content

Erdős problem 316

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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/316.lean

Formal Conjectures

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

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:316
  • PLBY Lean proofsErdosProblems.Erdos316

Continue

Search problems.science

Find a Problem, Result, source, or page