Let $N \geq 1$ and let $k (N)$ denote the smallest $k$ such that there exist $N \leq n_{1} < \dots < n_{k}$ with $1 = \frac{1}{n _{1}} + \dots + \frac{1}{n _{k}} .$ Is it true that $N \to \infty lim k (N) - (e - 1) N = \infty ?$

Open problem — our best result is machine-sealed: verified reduction, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · formalized (Lean) · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

verified reduction

needs verification

Transfer from #306: exact k(N) (min unit fractions summing to 1 with all denominators >=N) for N=1..11 = [1,3,5,8,10,11,13,15,17,19,21] (Opus-verified); PROVED k(N) finite for every N; frontier 22<k(12)<=24.

#306 denominator-floor control via identity-preserving refinement. Helper theorem (proved): maximal harmonic block N..M-1 below 1, then greedy exact tail with denominators >=M => k(N) finite for all N. Verified the exact table (witnesses sum to 1, all denoms>=N, term count=k). SCOPE: finite table + finiteness proof; does NOT prove the asymptotic k(N)-(e-1)N claim.

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **open** (as of the current literature I can find).

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 11 · textbook (literature)

lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k.succ → ℕ),
    (∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1

formal-conjectures/295.lean ↗

oeis

A192881 — Number of terms for the shortest Egyptian fraction representation of 1 starting with 1/n.1,3,5,8,10,11,13,15,17,19,21,23,25,26,28,30

links

related: #306

status