The board / number theory / #206
Erdős Problem #206
DISPROVED LEANdatabase updated 2026-04-28
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The Egyptian fraction sum: `∑_{m ∈ S} 1/m` for a finset of natural numbers.
`S` is an Egyptian underapproximation of `x`: valid denominators (all positive) and sum < x.
`S` achieves the best `n`-term Egyptian underapproximation of `x`, i.e. `egyptianSum S` realises \(R_n(x)\).
Let \(x>0\) be a real number. For any \(n\geq 1\) let \[R_n(x) = \sum_{i=1}^n\frac{1}{m_i}<x\] be the maximal sum of \(n\) distinct unit fractions which is \(<x\). Is it true that, for almost all \(x\), for sufficiently large \(n\), we have \[R_{n+1}(x)=R_n(x)+\frac{1}{m},\] where \(m\) is minimal such that \(m\) does not appear in \(R_n(x)\) and the right-hand side is \(<x\)? (That is, are the best underapproximations eventually always constructed in a 'greedy' fashion?) Kovač [Ko24b] has proved that this is false - in fact as false as possible: the set of \(x\in (0,\infty)\) for which the best underapproximations are eventually 'greedy' has Lebesgue measure zero.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/206.Prizenone
Topicsnumber theory, unit fractions
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/206
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.