#488: the density of multiples can more than double — Gessel's counterexample holds and its Lean replays clean, and certified explicit counterexamples bring n down from about 10¹¹⁸ to 2⁶⁴ in his own family and to 1.1·10¹⁵ in one of Liu's bands

The problem (erdosproblems.com/488; Erdős 1961, 1966 p. 150, 1980 p. 112; Guy's Unsolved Problems in Number Theory, E5). Let A be a finite set of integers ≥ 2, let B be the set of positive multiples of members of A, and let M(x) count the members of B up to x. Is it true that M(m)/m < 2·M(n)/n whenever m > n ≥ max A? The 2 cannot be lowered: A = {a}, n = 2a − 1, m = 2a gives a ratio of 2 − 1/a. Two of Erdős's printings say "non-multiples"; that misprint has its own small counterexamples (Cambie; Alexeev and Aristotle, November 2025), which say nothing about the multiples version asked here.

Where it stands.

• 5 September 2026. Declan Gessel, working with OpenAI's GPT-6 Astra, posted a counterexample: A = the integers in (T, 256T] whose prime factors are all below 257, with T = 256^k for some k < 4096 found by pigeonhole, n = 256T and m = 2TQ (Q = the product of the odd primes below 257). It was checked in Lean on the Jig platform (problem 398, statement 40), posted as a proof claim on erdosproblems.com, and sent to Formal Conjectures as PR #5297.
• Since then. On Jig, C. Benefield showed that the ratio can exceed 3 and is unbounded (statements 42–43), and woshuajolk certified an explicit instance with T = 2³⁸⁴, so n ≈ 10¹¹⁸, with a Python checker (statement 41). Dylan Z. Liu's preprint (Zenodo, 17 Oct 2026, not peer-reviewed) treats the question as settled and finds the sharp order of the largest possible ratio. A Formal Conjectures maintainer labelled the PR "solution found", and a reviewer replayed its Lean. Carlos Toledo's note of 7 November certifies the Lean again.
• What the trackers say on 11 November. Jig marks the problem refuted. erdosproblems.com has shown no problem statuses since 6 October, and its remarks on #488 (last edited 8 April) do not mention the counterexample; the proof claim has no comments. The community database lists #488 as "falsifiable", which it defines as open. Formal Conjectures still tags erdos_488 research open; PR #5297 is unmerged and needs a rebase.
• The smallest counterexample is open: it is Liu's Problem 18. As far as we found, no explicit counterexample with n below about 10¹¹⁸ had been published. Liu reports that one band with n = 6.7·10¹³ reaches only 1.447. Our own July search (every reduced A with max A ≤ 28, every m ≤ 10⁶) found nothing, as the sizes below explain.

Labels: (a) elementary proof · (d) established by computation, reproducible from our bundle.

Our referee pass: the counterexample holds. The checks below were done by Claude instances, not by human mathematicians.

• The mathematics. A separate Claude instance, briefed only with Gessel's note and told to act as a hostile referee, tried to break every step and found no gap. Write H(j) for the number of odd 251-smooth integers up to 256^j. It checked that the multiples of A up to n are exactly A (a cofactor below 256 has only small prime factors); the bound |A| ≤ 8H(k+1); the injection that gives M(m) ≥ H(k)·φ(Q), which also works for even residues; the pigeonhole; and the constant 3Q < 16φ(Q) (φ/Q = 0.2007). Each counting lemma has a positive control at the real parameters and a negative control that breaks one hypothesis and fails as it should.
• The Lean. We replayed it on our own machine (Lean 4.33.0, Mathlib db584cd): it compiles, and both the Jig theorem and the adapter to Formal Conjectures depend only on propext, Classical.choice and Quot.sound.
• The statement. We pasted the current erdos_488 statement from Formal Conjectures (fetched 11 November, after its 14 October change that removed the prop-valued answer) into the same file, proved it definitionally equivalent to Gessel's adapter by Iff.rfl, then proved its negation. Three planted errors were caught: a false constant fails, a planted sorry shows up in the axiom list, and changing the 2 to a 3 breaks the bridge. One caveat: this was elaborated with the file's own Mathlib imports, not inside a Formal Conjectures checkout.
• Two wording fixes to Gessel's note. Jig's "exact negation" is of Jig's own restatement, which omits 1 ∉ A; Formal Conjectures' statement is refuted through Gessel's adapter. And the note's "the problem is closed" means closed on Jig.
• The pigeonhole's k can be named. The note says the proof "does not compute" k. The smallest k its condition 2H(k+1) ≤ 3H(k) accepts is k = 111, and k = 110 fails it; the referee instance bracketed H(k), numbers near 10⁴⁹, in exact integer arithmetic. So Gessel's own argument certifies T = 2⁸⁸⁸ at the earliest.

The tool: an exact count of the multiples. Take P = the primes up to y, let q be the next prime, pick Λ with y ≤ Λ ≤ q, and let A be the P-smooth integers in (T, ΛT] with n = ΛT. Liu (Lemma 12) shows that an integer is a multiple of A exactly when its P-smooth part exceeds T. So, with Ψ(x) the number of P-smooth integers up to x, "rough" meaning no prime factor ≤ y, and m = WT:

M(n) = |A| = Ψ(ΛT) − Ψ(T),    M(WT) = Σ_{rough u < W} (Ψ(WT/u) − Ψ(T)).

We keep W < q², so the rough u < W are just 1 and the primes in [q, W). We re-checked both formulas by sieving every multiple directly in 86 small cases, 24 of them with Λ < q (0 mismatches; deliberately broken versions fail). Gessel's construction is the case y = 251, Λ = 256: Liu writes it as p = 257, but with Gessel's primes below 257 it is y = 251, inside the lemma. Everything is now a count of smooth numbers, and the question becomes how small T can be.

Ours: explicit certified counterexamples (d). We bound Ψ above and below by counting exponent vectors against integer weights ⌊2²⁰ ln p⌋, by dynamic programming in exact 128-bit integers. Rounding each weight down can only overcount, which gives the upper bound. Each floor loses less than one unit per prime factor, so shrinking the threshold by the factor w/(w+1), with w = ⌊2²⁰ ln 2⌋, gives the lower bound. A pair is certified when n · (lower bound on M(m)) > 2m · (upper bound on |A|), compared as exact integers. (For the whole-period row, M(m)/m is the density of B, bounded below by a tail sum in extended precision with a rounding allowance; see the bundle README.)

	y, Λ	T	n = ΛT	m	certified ratio ≥	second program: ratio ≥
Gessel's own inequalities, smallest k his pigeonhole accepts (k = 111)	251, 256	2888	2896	2889·Q	2.14	—
Explicit instance on Jig (statement 41, woshuajolk; Python checker; not ours)	251, 256	2384	2392 ≈ 1.0·10118	2385·Q	> 2	—
Gessel's set, whole period (certificate ours)	251, 256	264	272 ≈ 4.7·1021	lcm A	2.0467	—
Gessel's set at k = 7 (certificate ours)	251, 256	256	264 ≈ 1.8·1019	22,616·256	2.1253	2.1254
Liu's 1009-band at T = 1.2·1012 (certificate ours)	1009, 1013	1.2·1012	1,215,600,000,000,000 ≈ 1.2·1015	250,347·T ≈ 3.0·1017	2.0036	2.00364 (true value in [2.00364, 2.00366])
Smallest certified by both programs (certificate ours)	1009, 1013	1,096,478,196,143	1,110,732,412,692,859 ≈ 1.11·1015	251,224·T	2.00028	2.00036 (true value in [2.00036, 2.00038])

A is always the set of integers in (T, ΛT] with no prime factor above y; Q is the product of the odd primes below 257. The ratio is (M(m)/m) ÷ (M(n)/n); Erdős asked whether it is always below 2. The set at T = 1.2·10¹² has about 5.7·10¹¹ elements, all above 1.2·10¹². Its multiples up to n are just A, a fraction 4.7·10⁻⁴ of [1, n]; up to m they are at least a fraction 9.4·10⁻⁴ of [1, m]. Liu's Table 1 gives this band's limiting ratio as 14.47 as T → ∞; at T = 1.2·10¹² it is only just above 2, which is why the certificate needs exact counts. Smallest certified n by y on our grid: 199: 5.9·10¹⁷; 251: 8.1·10¹⁶; 307: 2.0·10¹⁶; 401: 5.0·10¹⁵; 449: 4.1·10¹⁵; 523: 1.9·10¹⁵; 557: 1.6·10¹⁵; 887: 1.20·10¹⁵; 1009: 1.11·10¹⁵; 1129: 1.21·10¹⁵; 1327: 1.13·10¹⁵; 1499: 1.38·10¹⁵; 1999: 1.59·10¹⁵. The best m is about 80 to 400 times n. For Gessel's set at k = 6 (T = 2⁴⁸), the m with our best lower bound, 24,415·2⁴⁸, has ratio in [1.99468, 1.99470] (second program), just short; the other m we tried (W from 32·257 to 66,048 in steps of 257) have lower lower bounds, and we have not ruled out every m.

How we know the counts are right.

• Exact counts by a different algorithm. A separate program enumerates the smooth numbers through a table of 5-smooth numbers and a parallel tree search. We tested 9 points: y = 251 at T = 10, 10⁴, 10⁶, 10⁸; y = 509 at 10¹⁰, 10¹²; y = 61 at 10⁵, 10⁶, 10¹². Every exact value lies inside our bounds and every certified ratio is below the exact one. For the finite-m certifier, tested on Liu's y = 61 band, the gap is about 4 parts in 10⁵.
• Liu's printed number. For y = 61, Λ = 67, T = 10¹², we get |A| = 64,844,856 exactly, as Liu prints. With m = 2876·T, that band's exact ratio is 1.5242, above the 1.447 Liu reports as the largest found for it. That m may lie outside the range he searched; the band's whole-period ratio is 1.4438.
• A planted error. Our certifier with every weight rounded up instead of down undercounts a known exact value, so the containment check can fail.
• A second implementation. A separate Claude instance wrote its own certifier without seeing our code, from the definitions and Liu's identity, which it re-checked by brute force on small cases. It uses different weights (rounded to nearest, at two resolutions), a different error model, and uint64 counts. It passed its own containment and planted-error controls. It certifies every row with an entry in the last column, with two-sided brackets there. For Gessel's set at k = 6 with m = 24,415·2⁴⁸, its upper bound is below 2 (ratio in [1.99468, 1.99470]), so that pair is not a counterexample.

What this does not do. We do not claim these are the smallest counterexamples: Liu's Problem 18 stays open, and our numbers are upper bounds for it, found on a grid of T and m within one family of bands. The certificates are computer-assisted, not Lean proofs; a Lean version would have to formalise counts up to about 3·10¹⁴ (smooth numbers up to about 3·10¹⁷). The counterexample itself, and the problem's resolution, are Gessel's. The bands with y = 1009 are among those in Liu's Table 1; what is ours is a finite T and m at which they provably work.