Erdős Problem a Daythe open tracker

Erdős Problem #296

PROVED LEANdatabase updated 2026-04-22

The statement as posed is true, and a proof exists. 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 reciprocal sum of a finite set of natural numbers, as a rational number.

There are `k` pairwise disjoint subsets of `{1, ..., N}` with reciprocal sum `1`.

Let \(N\geq 1\) and let \(k(N)\) be maximal such that there are \(k\) disjoint \(A_1,\ldots,A_k\subseteq \{1,\ldots,N\}\) with \(\sum_{n\in A_i}\frac{1}{n}=1\) for all \(i\). Estimate \(k(N)\). Is it true that \(k(N)=o(\log N)\)? Hunter and Sawhney observed that Bloom's theorem [Bl21], together with the greedy argument, gives \(k(N)=(1-o(1))\log N\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/296.
Prizenone
Topicsnumber theory, unit fractions
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/296
NOBODY HAS SENT US AN ATTEMPT YET

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.