---

Claim. Every natural number is a finite sum of distinct unit fractions whose denominators are each the product of two distinct primes (Theorem 1.2 of the preprint, p. 2). More generally, for $b$ squarefree let $N_b$ be the index of the largest prime factor of $b$ in the sequence of primes and let $B_N=\sum_{i<j\le N}1/(p_ip_j)$; then every $a/b$ with $a/b\ge\min\{B_{N_b}/6,1/5\}$ has such a representation (Theorem 7.1, p. 12, and Theorem 7.4, p. 14). The threshold is $1/5$ once the largest prime factor of $b$ is at least $59$. The preprint also proves, for every $k\ge3$, that every positive rational with squarefree denominator is a sum of distinct unit fractions whose denominators have exactly $k$ distinct prime factors (Theorem 8.1, p. 14, and Corollary 8.6, p. 17); the preprint thereby claims the three-prime statement which the 1980 monograph calls proved but unpublished, but that concerns a different denominator class and is not part of this claim.

Submission note. Posted to the site's forum by Shisheng Li on 18 June 2026:

I have a proof of the omega=2 case of this problem, formalized in Lean 4 / Mathlib. Below is a summary of the argument, followed by a link to the formalization.

Disclosure. This is a human-AI collaboration. I directed the mathematics and take full responsibility for all content; AI tools (principally Anthropic's Claude, used through Claude Code) contributed substantially to the Lean 4 / Mathlib formalization, to the numerical experiments, and to parts of the exposition. The arXiv version states this explicitly, both in the abstract and in a dedicated "Use of AI" section.

Summary of the proof.

In their paper BEG15, they proved the $\omega=3$ case: every natural number can be written as a sum of finitely many distinct unit fractions whose denominators are each a product of three distinct primes.

We reuse the proof machinery of BEG15, only with the target being the $\omega=2$ case, i.e. requiring the denominator of each unit fraction to be a product of two distinct primes -- that is, the denominators are so-called semiprimes.

This machinery reduces the problem to whether a natural number $n$ is a member of the set $L^2(N)/P_N$, where $P_N$ is the primorial of $N$, and the former, $L^2(N)$, is the set of all possible sums of the atoms $P_N/p_i/p_j$; its largest element is $\sigma^2(N)$ (note that this value equals $B_N\cdot P_N$, where $B_N=\sum 1/(p_ip_j)\to\infty$, so it is far larger than $P_N$).

The machinery then converts this problem into a contiguous-covering problem for the middle segment of $L^2(N)$ within the interval $[0,\sigma^2(N)]$, and proves that for $N\ge 10$ the interval $[\lceil \tfrac16\sigma^2(N)\rceil,
\lfloor \tfrac56\sigma^2(N)\rfloor]$ is always covered; after normalizing these intervals by dividing by $P_N$, their union covers the whole of $[1,\infty)$, so every natural number $n$ can be expressed, which proves the $\omega=2$ case.

To prove the central-covering problem above, we use an inductive argument. For $N$, multiplying its covered interval by $p_{N+1}$ yields a comb inside $L^2(N+1)$ whose elements are spaced $p_{N+1}$ apart, and these elements are also elements of $L^2(N+1)$. Then, via Olson's theorem, we prove the completeness, over the finite field $\bmod\ p_{N+1}$, of the atoms of $L^2(N+1)$ of the form $P_{N+1}/p_i/p_{N+1}$ -- i.e. the fillability of the gaps of the comb -- thereby advancing the central covering from $N$ to $N+1$.

The argument above extends quite naturally to part of the rational case. For a fraction $a/b$ in lowest terms with $b$ squarefree, as long as $a/b$ is not too small, multiplying it by some $P_N$ lets it fall into the corresponding central covering region, and so we obtain the required sum representation. But if $a/b$ is too small, it cannot fall into any such central region and the argument fails; this is why our proof does not cover all rationals. We prove a lower bound: for every $a/b>1/5$, a suitable $P_N$ can be found. With this in hand, the rational $\omega=3$ case becomes easier instead, because for any $a/b$ we can simply multiply by a large prime $r$ so that $a/b\cdot r>1/5$, then decompose it into a sum of reciprocals of semiprimes, and finally divide each reciprocal by $r$, thereby obtaining a sum of reciprocals of products of three primes -- this is the rational $\omega=3$ case. There is, however, one issue to resolve: we require $r$ not to coincide with a prime factor of the semiprimes, i.e. to avoid the situation $1/(r\cdot r\cdot p)$; in the paper this is handled by restricting the central-covering argument from $P_N$ to the primorial that excludes $r$, together with the corresponding sets. For the $\omega\ge 4$ case, our lifting technique can be obtained similarly from $\omega-1$.

This is the rough outline of the entire proof.

Formalization. The complete Lean 4 / Mathlib formalization (and the standard-library Python scripts) is included in the arXiv source tarball, downloadable here: https://arxiv.org/src/2606.15159 (the 'anc/lean/' directory). The entire development is machine-checked, with no 'sorry'. It reduces to exactly two explicitly cited classical inputs -- Olson's addition theorem and a Rosser-type prime bound -- together with the standard Lean/Mathlib foundations and the 'native_decide' compiler-trust base used for the finite computations; the full axiom surface is listed in the appendix and can be inspected with '#print axioms'. A full build takes on the order of ten minutes.

Preprint: https://arxiv.org/abs/2606.15159

Shisheng Li

Covers. The case $b=1$ of Problem 306, every natural number, and every $a/b$ with $b$ squarefree and $a/b\ge\min\{B_{N_b}/6,1/5\}$, with $B_N$ and $N_b$ as above. The rationals below the threshold are not covered: Section 9 (p. 19) reduces them to the preprint's Conjecture 9.1, that the gap-free floor $\gamma_N$ of the subset sums of $\{1/(p_ip_j):i<j\le N\}$ tends to zero, and its Proposition 9.2 shows that the conjecture would give the whole statement.

Route. The proof adapts the induction of Butler, Erdős and Graham for three prime factors (their Theorem 1) to two. The induction step reduces to an explicit inequality between the onset of the subset-sum interval at stage $N$ and two bounds, proved for every $N\ge10$ through Olson's addition theorem and Chebyshev-type bounds above a finite base range that is checked by machine; three ingredients are exact finite computations (Section 1.4).

Standing. Preprint only: Li, S., Every natural number is a sum of distinct semiprime unit fractions, arXiv:2606.15159, v1 of 13 June 2026 and v2 of 17 June 2026, 22 pages; no journal record, citing paper or independent review and no later arXiv version. The author announced the preprint in the site's discussion on 18 June 2026, disclosing a human--AI collaboration and summarizing the proof; the site's curator, Thomas Bloom, replied the same day that the preprint claims a partial result, many rationals including every integer, and not a proof of the whole problem; the site labels the problem OPEN (page last edited 21 June 2026, as of 2026-10-07). The preprint's statement on the use of AI (p. 22) says that the author directed the mathematics and takes responsibility for the content, and that AI assistants, Anthropic's Claude through Claude Code among them, contributed substantially to the Lean 4 formalization, the Python verification scripts and parts of the exposition. The arXiv submission carries that Lean development as ancillary files; the preprint describes it as free of sorry on two cited classical inputs (Olson's theorem and a Rosser-type prime bound) together with native_decide. This corpus has not built or audited it, so no formalized evidence is listed, and it has no posting apart from the arXiv submission. The same author's later preprint, on its own page Li's elementary proof of the full statement, asserts the whole statement by a different method and supersedes this result where it holds.