Erdős Problem #293
ambiguous statement

Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, log log v(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.