---

Claim. Every positive rational $a/b$ with $b$ squarefree is a finite sum of distinct unit fractions whose denominators are each the product of two distinct primes: the whole statement of Problem 306, answered yes. This is the theorem of the preprint Unit fractions with semiprime denominators: an elementary proof of Erdős Problem #306, arXiv:2609.32140, v1 of 26 September 2026, 13 pages, by Shisheng Li.

Submission note. Posted to erdosproblems.com as a proof claim by Shisheng Li (account daizisheng) on 29 September 2026, giving "GPT-5.6-sol, GPT-6-astra, Claude Opus 5.5" as the AI used:

Full proof of #306: every a/b > 0 with b squarefree is a finite sum of distinct 1/(pq), p ≠ q primes. After reducing to small targets, take one complete bipartite graph between V = {2} ∪ {primes of b} ∪ {primes in (y², 2y²]} and a tuned set U of primes in (y⁸, y⁹], and count subgraphs with reciprocal sum ≡ a/b (mod 1) by a finite Fourier sum. Small frequencies give a positive main term; all others are negligible by a divisor count and a no-wrap-around form of the CRT. The only inputs about primes are Chebyshev-type bounds. Lean formalisation: no sorry, standard axioms only. Notes: Problem: Erdős–Graham ask whether every a/b > 0 with b squarefree is a sum of distinct 1/(pq), p ≠ q primes. Earlier partial result (ours, arXiv:2606.15159): all natural numbers, and all a/b ≥ T(r) ≤ 1/5. Tang's Lean development (doi:10.5281/zenodo.20767390) gave the first full proof, conditional on two Rosser–Schoenfeld axioms. This proof uses Tang's circle-method framework, but a different construction (one two-scale bipartite graph) removes his anchor-synchronisation step and the Gaussian main term, and needs only Chebyshev bounds. So it is shorter and checkable by hand. Lean: no sorry, standard axioms only; also proves the formal-conjectures statement. (arXiv v1 still says the formalisation assumes Ramanujan's inequality; the repo now proves the needed bound.)

Route (as the abstract and the claim's summary describe it). After a reduction to small targets, the proof takes a single complete bipartite graph whose two sides are the set of primes in $(y^2,2y^2]$ together with $2$ and the primes dividing $b$, and a tuned initial segment of the primes in $(y^8,y^9]$; the denominators are the edges $pq$. The number of subgraphs whose reciprocal sum is congruent to $a/b$ modulo $1$ is written as a finite Fourier sum over frequencies indexed by the two sides. The small integer frequencies give a positive main term, and every other frequency is negligible by a divisor-counting bound and a form of the Chinese remainder theorem without wrap-around; since the total reciprocal mass is small, a subgraph with the right residue has sum exactly $a/b$. Chebyshev-type bounds are the only facts about primes the proof uses. The framework is taken from the circle-method argument of Tang's Lean proof, which the preprint credits with the first proof of the statement; the new construction, one bipartite graph on two scales, removes that argument's anchor-synchronization step. The sketch above is the author's, from the abstract and the claim's summary on the site.

Formalization. The repository's lean/ folder, at the pinned commit of 29 September 2026, declares erdos_306 (a finite set of semiprimes whose reciprocals sum to a given positive rational with squarefree denominator) and erdos_306_formal_conjectures, which the README describes as proving the proposition of the formal-conjectures statement file for the problem, and reports for both the axioms propext, Classical.choice and Quot.sound. The arXiv v1's ancillary Lean files kept one sorry, for the Chebyshev-type lower bound of the preprint's Lemma 2.1, which the paper cites as an inequality of Ramanujan; the repository's commit of 29 September 2026 proves the bound needed for large arguments from the central-binomial argument and removes the sorry. This corpus has not built or audited the development, so no formalized evidence is listed.

Standing. The site's proof-claims tab carries this as its one full proof claim, submitted 2026-09-29 by the author, who names GPT-5.6-sol, GPT-6-astra and Claude Opus 5.5 as the systems used; the abstract calls the work a human--AI collaboration in which AI tools contributed substantially to the construction, the experiments and the writing. The claim's three comments (29 September to 3 October 2026) are an exchange with Tang, who welcomes the proof, reports simplifying their own and publishes their August manuscript; none is a review. No refereed publication, independent review or acceptance by the site is recorded the arXiv listing shows v1 only and the site labels the problem OPEN (page last edited 21 June 2026,). The same author's earlier preprint, on its own page Li's semiprime representations of integers and large rationals, proved the case $b=1$ and the rationals above an explicit threshold by a different method; this claim supersedes it where it holds.