Skip to content

Erdős problem 316

Start work

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?

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 → ∑ 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

Proof manifests naming this Problem

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

Continue

Start a contributionBrowse the source filesOpen the collection entry