---

Submission note. Posted to the site's forum by Przemyslaw Chojecki on 20 March 2026:

I had a pretty long back-and-forth with GPT-5.4 about the problem, generally proving a bunch of special cases. I attach the full note with results here, but also check what the new Aristotle have done here when it comes to formalization (multiple files + readme).

It's pretty good on this problem which is elementary, but has tricky computations and notations that LLMs are worse at. I've done GPT-5.4 to Aristotle and back loop a couple of times too.

Also I couldn't find much literature when it comes to this problem.

The claim. For a finite nonempty $A\subseteq\{2,3,\ldots\}$ write $f_A(x)$ for the number of positive integers up to $x$ divisible by a member of $A$, $D_A(x)=f_A(x)/x$, and $A_{\min}$ for the primitive reduction of $A$, its members divisible by no other member. Theorem 1.1 of the note Signed Transport, Pair–Tail Reduction, and Low Layers in an Erdős Density-Doubling Problem, dated 20 March 2026: the inequality of Problem 488, $D_A(m)<2D_A(n)$ for all $m>n\ge\max A$, holds (a) when $|A_{\min}|\le3$, (b) when $f_A(n)-|A_{\min}|\le5$, (c) when $f_A(n)\le9$, and (d) for every $m>n$ once $n>(2W_+(A)+W_-(A))/\delta_A$, where $\delta_A$ is the density of the multiples of $A$ and $W_\pm(A)$ are the positive and negative parts of the signed inclusion--exclusion weights over the lcm values of the subsets of $A$; (e) a pair with $D_A(m)/D_A(n)>2-\varepsilon$ forces $n$ below a bound of the same shape. The method writes $f_A$ in the lcm basis and transports the signed weights from $n$ to $m$; splits the multiples of a pair of generators against a tail of further moduli, proving the doubling inequality for a singleton and for a pair against one forbidden modulus, which gives (a); and for (b) uses a union bound in the sparse regime, (c) following from (a) and (b). The note states two conjectures: Conjecture 4.8, a split doubling inequality for a pair of generators against a tail, which by its Proposition 4.9 would imply the problem for every finite $A$, and Conjecture 6.11, on order slack in the sparse regime; the manuscript on the shoal-rat page gives counterexamples to both and credits the excess-at-most-five theorem. The author's thread comment says the note came out of a long exchange with GPT-5.4 and that the results were verified by Aristotle and are in Lean, the archive linked above; that formalization is the claimant's and gives no formalized evidence, since nothing was built or audited here.

Covers. The problem's inequality for every finite $A$ whose primitive reduction has at most three members; for every $A$ and $n\ge\max A$ with $f_A(n)-|A_{\min}|\le5$, hence for every $A$ and $n$ with $f_A(n)\le9$; and for every $A$ at all $n$ above the note's explicit threshold. Not covered: the problem in general. The note names $f_A(n)=10$ with a primitive reduction of size four as its first unresolved layer, and the counterexample on Gessel's page has far more than three primitive elements and an excess far above five, so it lies outside every covered class.

Standing. Claimed. The note is linked from the author's comment of 20 March 2026 in the site's discussion thread, not from the proof-claim tab; a reply the same day reports that a check run with ChatGPT claimed one minor issue, and the author answered that the results were also verified by Aristotle and are in Lean. The site's label and commentary (last edited 8 April 2026) do not mention the note, and no referee or named reviewer is on record. Later thread work builds on it: MalekZ's reduction chain for Conjecture 4.8 (29 and 30 March 2026, recorded on the problem page), the $a=2$ case and the observation that the note's reduction to a fixed threshold fails for $a\ge3$ at thresholds below $\max A$ (31 March 2026), and the shoal-rat manuscript's extension of the excess bound from five to fifteen (5 September 2026).

Depends on. Nothing in this wiki: the claim rests on its own note.