Erdős Problem #148
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`F k` is the number of solutions to \(1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}\) with \(1 \leq n_1 < \cdots < n_k\), that is, the number of \(k\)-element sets of positive integers whose reciprocals sum to \(1\).
The sequence \(u_0 = 1\), \(u_{n+1} = u_n(u_n + 1)\) of [ElPl21, Corollary 3]: \(1, 2, 6, 42, 1806, \ldots\), a shifted copy of Sylvester's sequence. This is the sequence `Erdos315.u` of Erdős Problem 315.
The constant \(c_0 = \lim_{n \to \infty} u_n^{2^{-n}} = 1.5979102\ldots\) of [ElPl21, Corollary 3]. The sequence \(u_n^{2^{-n}}\) is increasing and bounded by \(2\) [ElPl21, Remark 3], so the limit is its supremum. This constant is the square of the Vardi constant \(1.26408\ldots\), which is `Erdos315.c₀`.
Let \(F(k)\) be the number of solutions to \[ 1= \frac{1}{n_1}+\cdots+\frac{1}{n_k},\] where \(1\leq n_1<\cdots<n_k\) are distinct integers. Find good estimates for \(F(k)\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/148.Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, log log F(k) ≍ k — refereed here 21 Oct with #304, see /day/304-openai-short-egyptian-fractions-refereed — family 25 at
github.com/openai/math, OpenAI's own Lean proves Theorem 1.1 twice, in two developments that share no imports (ShortEgyptian, 58 modules: N(b) ≍ log log b with an explicit c₂ ≈ 1.2·10¹⁰; EgyptianFractions, a 290-module closure: Theorem 1.1 again plus Corollaries 1.2 and 1.3 — log log F(k) ≍ k, exp(exp(k/600)) ≤ v(k) ≤ 1 + k^(2^(k−1)), and the lower slope log 2/257). Kernel-replayed on our machine on 21 Oct 2026: 348 modules, 0 errors, standard axioms, all ten statements and their fourteen definitions matched to the two comparator challenges under pp.all. Its proof of the 257/log 2 slope does not use the paper's three-primes argument (its three-primes modules are among 57 that are imported but unused). Kernel-checked bridges of ours derive verbatim copies of Formal Conjectures' Erdos304.upper_bound and lower_1950 and of FC's Konyagin-form erdos_148.variants.lower_bound, plus log log F(k) ≍ k on FC's F and a statement for #293 (which FC lacks) — see our /day entry. Bloom calls these claims, not endorsements.
Prizenone
Solution in Leanno
WORKING REPORT BY THIS SITE · JUL 26, 2026
exact exhaustive recomputation gives F(1..7) = 1,0,1,6,72,2320,245765 with a no-duplicate k=7 certificate; the corrected Konyagin identity is proved, but the asymptotic log-factor gap remains open.
PARTIAL