---

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. The claim is a Lean 4 development over Mathlib whose record describes its headline theorem as the proposition of the formal-conjectures statement file for the problem, complete apart from two inputs stated as axioms, the explicit prime-counting bounds of Rosser and Schoenfeld (1962). Those inputs are published theorems, so the claim is recorded as a full one and not as conditional; the development proves the statement only together with them, and this corpus has not built or audited it, so the identity of its headline theorem with the problem's statement rests on the author's description.

Submission note. Posted to the site's forum by Yuren Tang on 19 June 2026:

I would like to report a Lean-formalized affirmative solution to this problem.

The main theorem has been formalized in Lean 4 with Mathlib; the corresponding release is archived in Tang (2026). The formalization is sorry-free; apart from Lean’s standard logical axioms, the stated axiom boundary consists of two explicitly named inputs corresponding to Rosser and Schoenfeld (1962). A human-readable arXiv manuscript is currently being prepared.

Tang, Y. (2026). A machine-checked proof of Erdős Problem 306 in Lean 4 (v0.0.3). Zenodo. https://doi.org/10.5281/zenodo.20767390

Rosser, J. Barkley, and Lowell Schoenfeld. “Approximate formulas for some functions of prime numbers.” Illinois Journal of Mathematics 6(1): 64–94, March 1962. https://doi.org/10.1215/ijm/1255631807

Postings. The repository's releases are v0.0.1-prerelease (16 June 2026), v0.0.2 (18 June) and v0.0.3 (19 June 2026), the last archived on Zenodo as software under the DOI above (Apache 2.0) with the title "A machine-checked proof of Erdős Problem 306 in Lean 4"; the formalization link pins the commit of that release. The page is dated by that release and its announcement: the prerelease of 16 June describes itself as in progress and not yet a finished proof, and the prerelease of 18 June was superseded the next day by the first citable release. The author announced the release in the site's discussion on 19 June 2026 as a sorry-free formalization whose axiom boundary, beyond Lean's standard axioms, is the two named Rosser--Schoenfeld inputs, with a manuscript in preparation, and wrote on 20 June that the release is a verifiable snapshot of the formal result and not an exposition. The manuscript, Squarefree semiprime unit fractions: a characterization and a local limit theorem, was frozen on 11 August 2026 and made public on 3 October 2026 in the proof-claims thread of the site, at the commit the preprint link pins (an archived copy is cited there); the author writes that the proof has since been simplified, the major-arc and minor-arc machinery of the circle method removed, and that a revised manuscript is in preparation while an arXiv endorsement is sought. This page records the manuscript by its title, its dates and the author's description of it. The later preprint of Li, on its own page Li's elementary proof of the full statement, credits this development with the first proof of the statement, describes its framework as a circle-method argument with an anchor-synchronization step, and reuses the framework with a different construction.

Standing. No refereed publication, independent review or acceptance by the site is recorded as of 2026-09-18 and 2026-10-06; the site labels the problem OPEN (page last edited 21 June 2026, as of 2026-10-07), and the site's proof-claims tab carries no claim of the author's own, the manuscript appearing only in the comments on Li's claim. This corpus has not built or audited the development, so no formalized evidence is listed; the page rests on the release metadata of the Zenodo record and the repository.