---

Claim. Fix $r\ge2$ and call $A\subseteq\{1,\ldots,N\}$ admissible when every integer $m$ has at most $r$ representations $m=pa$ with $p$ prime and $a\in A$. Then the largest value of $\sum_{a\in A}1/a$ over admissible sets is $\Theta_r(\log N/\log\log N)$: Erdős's upper bound of this order, from the double count of the products $pa$ (display (4.5) of 1973, recorded on Problem 538), is matched by an admissible set whose reciprocal sum is $\gg_r\log N/\log\log N$. The claimant presents this as the best possible bound the problem asks for; the contribution claimed is the construction, the upper bound being known.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim the best possible bound is $\sum_{n\in A}\frac{1}{n}=\Theta_r\left(\frac{\log N}{\log\log N}\right)$: the weighted-incidence upper bound of this order is matched by a construction attaining it. Proved in Lean 4 / Mathlib, standard axioms only, no sorry. Idea: on a squarefree layer with $k$ prime factors, the condition "at most $r$ solutions to $m=pa$" becomes a hypergraph cap condition: among the $k+1$ facets of any $(k+1)$-set, at most $r$ are selected (for $r=2$, the daisy problem). Known constructions gave density about $1/k^2$; the missing factor $k$ was exactly the missing $\log\log N$. We build a cap-two family of density $\Omega(1/k)$: label vertices with finite-field data and select facets whose relation line is isotropic for a diagonal bilinear form; three selected facets would force a totally isotropic plane, impossible in odd characteristic by $0=B(w,w)=2abB(u,v)$. A counting argument gives density at least $1/(64k)$, and a weighted colouring transfers a Notes: The upper bound of this order was known; the contribution is the matching construction, which also closes the density gap in the $r=2$ daisy problem from $1/k^2$ to the optimal order $1/k$. Verify: unzip, build, then "#print axioms" on the final theorems gives exactly [propext, Classical.choice, Quot.sound].

Construction, as the claimant describes it. Restricted to squarefree integers with exactly $k$ prime factors, the hypothesis says that of the $k+1$ products obtained by deleting one prime from a $(k+1)$-set of primes, at most $r$ may belong to $A$; for $r=2$ this is the daisy problem. Earlier constructions select a proportion of about $1/k^2$ of the layer, and the factor $k$ lost there is the factor $\log\log N$ missing from the lower bound. The claimant selects facets by labeling the primes with finite-field data and keeping a facet when the line it determines is isotropic for a diagonal bilinear form; three selected facets of one $(k+1)$-set would span a totally isotropic plane, which the form does not allow in odd characteristic. A counting argument gives a selected proportion of at least $1/(64k)$, and a weighted coloring transfers the family; the tab's summary breaks off in that sentence. This page rests on the tab's summary, not on the write-up or the archive the tab links, and the argument is not checked.

Formalization. The tab's entry says the result is proved in Lean 4 with Mathlib, with no sorry and only the axioms propext, Classical.choice and Quot.sound, and links an archive to build. The formal-conjectures file for the problem (ErdosProblems/538.lean, a statement file and not a formalization of the claim) carries a variant erdos_538.matching_order, tagged research solved with a formal_proof attribute pointing at the file FinalMatchingOrder.lean in the repository williamjblair/lean-proofs (linked above at a pinned revision of 30 July 2026, the file added on 23 July 2026; the development sits in that repository's starfleet/erdos-538 directory). That repository is attributed to this claim through the formal-conjectures pointer, not by the claimant, whose tab entry links only the archive. The variant states, for $r\ge2$ and $N\ge2$, that every admissible $A$ satisfies $\log\log(N+1)\sum_{a\in A}1/a\le2r(1+\log(N^2))$ and that some admissible $A$ satisfies $\log(N+1)\le4+8192(\lfloor\log_2\lfloor\log_2N\rfloor\rfloor+1)\sum_{a\in A}1/a$, which is the matching order with explicit constants; its docstring says this "pins the order (up to the one iterated-logarithm factor) but not the best possible upper bound asked for". The repository's 44-line file proves erdos538_matching_order from two imported modules, whose proofs this page does not assess; nothing was built, kernel-checked or audited here, so the development is not counted as formalized, and the catalog's main statement erdos_538 stays research open with a sorry.

Scope. Full, as the tab labels it and as the claimant states it. The problem asks for the best possible upper bound; the claim fixes the order $\log N/\log\log N$ for each fixed $r$ with unspecified constants, while the formal-conjectures maintainers read the question as asking for the asymptotic size of the extremal sum, constant included, and judge the matching order not to answer it (the docstrings quoted under Formalization). Read as its source reads it (the problem page's Formulation), the question asks whether the order of Erdős's (4.5) can be improved for fixed $r$, and the claim answers it. A sharper constant or an asymptotic formula, which the formal-conjectures statement asks for, would be a further result. The claimed lower bound does not grow with $r$ (the formal-conjectures variant's lower bound is free of $r$), so the factor $r$ in (4.5) is not shown to be sharp.

Claimant. Colin Snyder (the site user coffeewithcolin), whom the tab describes as using an AI system, GPT 5.6 (custom harness); the write-up is on the site the tab links as its external proof link.

Standing. Claimed. The site's label is OPEN (page with no last-edited date), the claim's thread held no comments on 2026-10-06, the commentary does not mention the claim, and the community database records the problem open with no formal proof. No refereed version, independent review or acceptance by the site was found. The catalog's research solved tag on its variant is recorded above and is not read as acceptance of the mathematics by this corpus.

Depends on. Erdős's inequality (4.5), the upper bound of order $\log N/\log\log N$ that the construction matches.