The board / number theory / #294
Erdős Problem #294
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`HasUnitFractionSolution m N` says that \(1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\) for some integers \(m=n_1<\cdots<n_k\leq N\): the \(n_i\) form a finite set `s` whose least element is `m`.
\(t(N)\): the least positive integer \(t\) such that there is no solution to \(1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\) with \(t=n_1<\cdots<n_k\leq N\). The set of candidates contains \(N+1\), so `sInf` is a true minimum.
Let \(N\geq 1\) and let \(t(N)\) be the least integer \(t\) such that there is no solution to \[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\] with \(t=n_1<\cdots <n_k\leq N\). Estimate \(t(N)\). Solved by Liu and Sawhney [LiSa24, Theorem 1.6] (up to \((\log\log N)^{O(1)}\)), who proved that \[\frac{N}{(\log N)(\log\log N)^3(\log\log\log N)^{O(1)}}\ll t(N) \ll \frac{N}{\log N}.\] The unspecified \(O(1)\) exponent is the real number `K`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/294.Prizenone
Topicsnumber theory, unit fractions
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/294
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.