---

Submission note. Posted to erdosproblems.com as a proof claim by shoal-rat (project curator) (account Fevernop) on 29 September 2026, giving "GPT-6 Astra (OpenAI Codex)" as the AI used:

Let G be a finite primitive set, F_G(x) the count of integers up to x divisible by a member of G, and E_G(n)=F_G(n)-|G|. We prove that, when n>=max G and E_G(n)<=15, the auxiliary bound sum_{g in G} floor(n/g)+|G|<=2F_G(n) holds. It implies the original strict inequality F_G(m)/m<2F_G(n)/n for every m>n. The proof reduces a possible failure to finitely many quotient profiles and verifies complete certificates in Lean. We also show that excess 16 is the exact first point where this auxiliary bound can fail, using a primitive, collectively coprime example. This example still satisfies the original inequality. Related counterexamples in the paper concern auxiliary conjectures, not problem #488 itself. Notes: Full paper, Lean sources, and reproducibility materials: https://github.com/shoal-rat/erdos-488-lean . The claim is partial; the unrestricted problem is not resolved by this project.

The claim. For a finite primitive set $G$ of integers at least $2$ (no element divides another), write $F_G(x)$ for the number of positive integers up to $x$ divisible by a member of $G$, $I_G(n)=\sum_{g\in G}\lfloor n/g\rfloor$, and $E_G(n)=F_G(n)-|G|$, the excess, which counts the covered integers up to $n$ other than the members themselves. Theorem 1 of the manuscript: if $n\ge\max G$ and $E_G(n)\le15$, then $I_G(n)+|G|\le2F_G(n)$, and for nonempty $G$ the inequality of Problem 488, $nF_G(m)<2mF_G(n)$, holds for every $m>n$. The second statement follows from the first because $F_G(m)\le I_G(m)\le m\sum_{g\in G}1/g$ and $n\sum_{g\in G}1/g<I_G(n)+|G|$. Since a finite set and its divisibility-minimal subset have the same multiples, the theorem covers every finite $A$ whose minimal subset $G$ has $F_A(n)-|G|\le15$; the manuscript notes that replacing $|G|$ by $|A|$ here is not justified. Theorem 2 shows that $16$ is the least excess at which the auxiliary estimate $I_G(n)+|G|\le2F_G(n)$ can fail, with the witness $G=\{16,24,36,40,54,56,60,81,84,88,90\}$, $n=180$ ($|G|=11$, $F_G(180)=27$, $I_G(180)=44$), and that such failures exist with $\gcd(G)=1$, arbitrarily small covered density and arbitrarily large $n$; those sets still satisfy the problem's inequality, so the threshold limits the method, not the problem. The manuscript, Beyond the Slack Barrier: Lean-Verified Bounds and Counterexamples for Erdős 488, dated 5 September 2026, is published in a GitHub repository under the handle shoal-rat, whose README says that the handle names no person; it states that the work was prepared through an AI-assisted workflow with OpenAI Codex, and the tab names the system as GPT-6 Astra (OpenAI Codex). The repository was published on 5 September 2026 and the claim was submitted to the site's proof-claim tab on 29 September 2026 as a partial claim. Its further results, counterexamples to Conjectures 4.8 and 6.11 of Chojecki's manuscript of 20 March 2026 (the claim page Chojecki's note, whose excess-at-most-five theorem it credits) and unbounded ratios for auxiliary quantities, concern strengthened formulations and not the problem; the manuscript says so.

Covers. The problem's inequality for every finite primitive $G$ and every $n\ge\max G$ with $E_G(n)\le15$, and so for every finite $A$ whose minimal subset has that excess. Not covered: the problem in general, which the manuscript states it leaves unresolved. The counterexample claim on Gessel's page lies outside the covered range: in its set every even element above $2T$ is a multiple of a smaller element, so the excess of its minimal subset at $n=\max A$ is far above $15$.

Standing. Claimed. The site's label and commentary (last edited 8 April 2026) do not mention the claim, the tab entry has no comments, and no outside review was found; the tab's notice says that appearance there is no guarantee of correctness. The Lean file ExcessFifteenMain.lean at the pinned commit states erdos488_excess_at_most_fifteen with the hypotheses above and the conclusion n * multipleCount G m < 2 * m * multipleCount G n for every m > n, and the published axiom log reports only propext, Classical.choice and Quot.sound (Lean 4.33.1, Mathlib pinned); the file and the log are neither built nor audited for statement fidelity here, so the formalization is the claimant's and gives no formalized evidence.

Depends on. Nothing in this wiki: the claim rests on its own manuscript and Lean sources.