Skip to content

Erdős problem 45

Let k≥2k\geq 2. Is there an integer nkn_k such that, if D={1<d<nk:d∣nk}D=\{ 1<d<n_k : d\mid n_k\}, then for any kk-colouring of DD there is a monochromatic subset D′⊆DD'\subseteq D such that ∑d∈D′1d=1\sum_{d\in D'}\frac{1}{d}=1?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/45.lean

Formal Conjectures

FormalConjectures/ErdosProblems/45.leanErdos45.erdos_456 linesExact file
True ↔  ∀ (k : ℕ),    2 ≤ k →      ∃ n,        ∀ (colouring : ℕ → Fin k),          ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:45
  • PLBY Lean proofsErdosProblems.Erdos45

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page