Erdős Problem 287

Exercise 287 · Erdős

The example $1 = \frac{1}{2}+\frac{1}{3}+\frac{1}{6}$ shows that $3$ would be best possible here: the sequence $(2, 3, 6)$ is a valid Egyptian fraction representation of $1$ with max_gap = 3.

Formal statement · Lean 4.lean

theorem erdos_287.test.best_possible :
    let s : Fin 3 → ℕ := ![2, 3, 6]
    StrictMono s ∧
    1 < s 0 ∧
    ∑ i : Fin 3, 1 / (s i : ℝ) = 1 ∧
    max_gap 3 s = 3 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗