#708: Haoyu Chen's g(n) ≤ 12n checks out and replays here, his threshold-2 barrier needs a bigger example, and his 3n/2 family exists at every size, so g(n) ≥ ⌊3n/2⌋ − 1 for every n ≥ 4 (a record only at small n)

The problem (erdosproblems.com/708; Erdős and Surányi 1959; Erdős 1992). Take integers 1 < a₁ < … < a_n and any run of a_n consecutive integers. Some of those integers have a product divisible by a₁⋯a_n; let g(n) be the number you need in the worst case. Is g(n) ≤ (2+o(1))n, or even ≤ 2n? Erdős offered "100 dollars or 1000 rupees, whichever is more". Gallai observed g(2) = 2. Erdős and Surányi proved g(3) = 4 and g(n) ≥ (2−o(1))n. A forum comment (May 2026) notes that the page's "|B| = g(n)" has to be read as "at most g(n)"; everyone below uses that reading.

Where it stands.

• Upper bounds. Erdős and Surányi gave no upper bound beyond g(3) ≤ 4: "we don't know whether the ratio can be substantially worse" (1959, in Hungarian). Haoyu Chen's manuscript (Zenodo v14, 8 Sep 2026; GitHub) gives the first upper bounds that depend on n alone, as far as he or we could find. GPT-5.6, GPT-6 and Qwen found its proofs, and a Claude orchestrator ran the pipeline, with Claude referees. It is posted as a proof claim on the problem page, with no outside comments (new comments are suspended site-wide). Successive versions bring the bound down from about n log₂ n, through O(n log log n), 81n, 33n and 19n, to 12n, checked in Lean 4. A further 11n was refereed but not formalised: as of his last commit (12 October) the Lean proves only that Section 18's inequality implies 11n; the inequality itself is not formalised. Chen also proves that 2n always suffice when max A ≥ 8n³. His method goes through linear-programming duality: a bound of about (c + 2)n follows from a "hinge inequality" with threshold c, which compares how often the prime factors of interest pile up on single integers in [1, m] and in the run. He argues that the threshold cannot go below 2 (see the slip below).
• Since then, on GitHub only. Ziming Wang (21 Oct) states g(n) ≤ 10n, and 8.83n + o(n), both on top of Chen's unformalised Section 18, and 2n once max A ≥ 16n². Notes written by Claude Fable 5.1, directed by Dovid Preil (15 Oct) rediscover two of Chen's results and write out the proof of the 1959 lower bound. Erdős and Surányi took every product p_ip_j with i, j = 1, …, ℓ, squares included (the problem page says i ≠ j), so n = ℓ(ℓ+1)/2, and counted ℓ(ℓ−1)+1 = 2n − 2ℓ + 1 integers needed. Beyond these two repositories we found no paper, preprint or forum post with another bound, and no replay of Chen's Lean by anyone else; his CI is green.
• Lower bounds and small values. Asymptotically the best is still Erdős–Surányi's (2−o(1))n. The 1959 paper's Theorem IV already gives g(n) ≥ n + 1 for every n ≥ 3; Chen re-derives g(4) ≥ 5 and g(5) ≥ 6 by computation. The repository version of his paper (§19, not on Zenodo) adds a family needing 3t − 1 integers at n = 2t, found by the referee instance in his pipeline and exhibited for t ≤ 6, so g(10) ≥ 14 and g(12) ≥ 17. Our own July–August rounds on this problem (/day/708-valuation-cover-c4) worked on the companion constant c_n, the interval length that guarantees n picks (c₄ = … = c₁₁ = 2). They left g(4) = 5 as a conjecture.
• Trackers on 12 November. The community database lists #708 as open and not formalised. Formal Conjectures has no file for it: PR #4388 was approved on 5 October and has been waiting on its author since 8 October.

Labels: (a) elementary proof · (b) rigorous, using a named theorem · (d) established by computation, reproducible from our bundle.

Our referee pass on the 12n claim. The checks below were done by Claude instances, not by human mathematicians.

• The statement says what Erdős asked. The sentence the Lean proves is Erdos708Statement.g_le 12, in a file that imports only Mathlib: for every finite set A of integers ≥ 2 with maximum M and every x ≥ 0, some B ⊆ {x+1, …, x+M} with |B| ≤ 12|A| has ∏B divisible by ∏A. That is g(n) ≤ 12n under the "at most" reading. Restricting to x ≥ 0 loses nothing: a run containing 0 is trivial, and a run of negative integers is the negative of a positive one. Two short theorems in FinalCheck.lean derive it, and g_le 19, from the project's own g_le_12n and g_le_19n.
• The kernel replay. We rebuilt the project on our own machine from Chen's commit dc150fd, with Lean 4.34.0-rc1 and Mathlib de5ce8a9. Mathlib's compiled files came from its public cache. All 180 of the project's own modules were compiled here from source, so our Lean kernel checked every proof in them. Most of the three hours went to the 16 modules that hold the 29 numeric certificates, some of which need 25 GB of memory each. The final check, FinalCheck.lean, printed nothing. Each of its axiom checks pins the exact output of #print axioms, so all of them held. g_le_12n, hinge97 and the Mathlib-only statement depend only on propext, Classical.choice and Quot.sound, and so does long_interval, whose axioms were printed during the build. No sorry appears anywhere in the build, and no native_decide appears in the source. As a control, a copy of the final check with one axiom list deliberately wrong fails. Chen's own CI passed the same check (run 38165611266 from a cold start, run 38187931698 at the current commit). We did not run leanchecker --fresh, so Mathlib's own files were taken from the cache on trust, as in every replay we report.
• A hostile referee instance was briefed to break four things. It broke no theorem and found one slip.
  • The long-interval theorem. 2n suffice when max A ≥ 8n³ (Chen's Theorem 1.3). The proof holds. Its Lean form, long_interval, states exactly that, and it lies among the files the final check depends on, on the path to g_le_81n; the 12n chain uses a different split. The referee's own exact solver found no instance above 2n in 4,055 tries with n = 2, 3, including 55 adversarial ones.
  • The arithmetic of Section 17. All 29 scales were recomputed from the printed formulas in exact arithmetic. The total lies in [186024001631, 186024001632]·10⁻¹², below 187/1000, and the window value is exactly 718539/573440 > 5/4.
  • The statement. Its reading agrees with ours above.
  • The barrier at 2 (Proposition 18.9 and Remark 18.10): the slip, below.
• One slip, in the barrier. Proposition 18.9 is correct as stated. It takes 21 primes from 503 to 641, a run of length 631·641 = 404,471 centred on their product, and threshold c = 19/10, and counts each integer's cluster primes once, so a prime square counts once and adds nothing; there 21 > 20. But Remark 18.10 then says the hinge inequality itself cannot go below 2, and the inequality the reduction actually uses (Chen's Theorem 16.1, and the Lean bound_of_hinge) is a different form. It counts w_z(k) = Σz_p·v_p(k), where v_p(k) is the exponent of p in k and the z_p are weights between 0 and 1, so a prime square counts twice. On the same 21 primes that form gives 23 on the left and 46 on the right, and the example does not break it. More primes do. On the 60 consecutive primes from 1049 to 1483 it gives 182.9 > 145. The referee found this, and we recomputed both examples with our own code. So the floor of 2 on the threshold stands, with a different example. Through Chen's (c + 2)n conversion that means this route gives nothing below 4n; through his asymptotic conversion (the one that turns threshold 17 into 18n + o(n)) the floor is (3 + o(1))n, as Ziming Wang's audit points out.
• The small values, recomputed. We wrote our own exact solver (it does not use Chen's dynamic programme). It treats integers that carry two or more of the needed prime factors (counted with multiplicity) by an exact search and fills the rest with interchangeable single multiples. On 400 random small instances it agrees with plain subset enumeration, and two planted bugs are caught 258 and 392 times out of 400. It reproduces all four instances the paper prints: A = {10, 12, 15, 20} with x = 50 needs 5; {5, 10, 12, 15, 20} with x = 50 needs 6; Chen's K_2,2 instance (primes 59, 61; 71, 73; x = 18,652,287) needs 5; the K_2,3 instance (67, 73, 79; 97, 101; x = 3,785,449,127) needs 8.

Ours: the 3n/2 family exists at every size (a), (b), (d). Chen's Section 19 (repository version) has a family that needs about 3n/2 integers, found by the referee instance in his pipeline. Take primes w₁ < … < w_t < q_u < q_v and let A be the 2t products w_iq_u, w_iq_v; each w_i is joined to both q's, which is why it is called K_2,t. If the run can be placed so that one integer, a multiple of every one of these primes, is the only member divisible by two of them, and no member is divisible by q_u² or q_v², then exactly 3t − 1 integers are needed. The paper exhibits such placements for t = 2, …, 6 and says a consequence would follow "if the placement exists for every t — which we have not proved". (The referee instance had asserted that consequence earlier, without a proof.) In Chen's statement the special integer is the product Π of the primes itself, and for some choices of primes no run works. His count goes through unchanged when the special integer is any multiple kΠ with k prime to all the primes, and choosing k by congruences pushes the multiples of q² out of the run. That device, a multiple of the product chosen to sit far from the square multiples, is Erdős and Surányi's own (their §4 and §9). What is ours is applying it to this family, which closes the gap Chen left open.

Lemma. Let t ≥ 2 and suppose m = w_tq_v (the largest member of A) is less than 2w₁w₂ and q_u² ≥ m + q_u. Then some run of length m needs at least 3t − 1 integers for A, and at least 3t for A ∪ {q_u}.

Proof. Centre the run on u = kΠ, from u − ⌊m/2⌋ to u + m − 1 − ⌊m/2⌋. For q = q_u or q_v, the offsets the run does not cover form q² − m consecutive residues mod q². That is at least q: for q_u by hypothesis, and for q_v because q_v² − m = q_v(q_v − w_t). So they contain a multiple qs of q, and s ≢ 0 (mod q) because offset 0, u itself, lies inside the run. (The second hypothesis gives q² > m, so a run of length m holds at most one multiple of q².) Choose k by the Chinese remainder theorem so that −u ≡ qs (mod q²) for both q, and so that k is prime to every w_i; since s ≢ 0 (mod q), k is prime to q as well. Then no member of the run is divisible by q², and each needed prime divides u exactly once. Any other member divisible by two needed primes p, p′ would differ from u by a non-zero multiple of pp′ ≥ w₁w₂, but every member is within m/2 < w₁w₂ of u. So each member other than u is divisible by at most one of the primes, and by q_u or q_v at most once. Now q_u and q_v are each needed t times and each w_i twice. A cover that uses u needs u, t − 1 more multiples of each q, and one more multiple of each w_i, all different: 3t − 1. A cover without u needs t + t + t = 3t. Adding q_u to A raises its demand to t + 1, so both counts go up by one. Both bounds are attained: the run holds at least t + 1 multiples of each q and at least two of each w_i. ∎

Theorem. g(n) ≥ ⌊3n/2⌋ − 1 for every n ≥ 4. To get the primes, use the prime number theorem: for large X there are t primes in [X, 1.2X) and two in [1.3X, 1.32X). Then m < 1.584X² < 2w₁w₂, and m + q_u < 1.69X² ≤ q_u² once X ≥ 13. This is label (b): rigorous, using the prime number theorem. For t ≤ 14 (n ≤ 29) explicit primes do it without that theorem, and our solver finds each value exact:

t	w1, …, wt	qu, qv	run length m	n = 2t: needed	n = 2t+1: needed
2	29, 31 (2 primes)	37, 41	1,271	4: 5	5: 6
3	53, 59, 61 (3 primes)	67, 71	4,331	6: 8	7: 9
4	53, …, 67 (4 primes)	71, 73	4,891	8: 11	9: 12
5	59, …, 73 (5 primes)	79, 83	6,059	10: 14	11: 15
6	79, …, 103 (6 primes)	107, 109	11,227	12: 17	13: 18
7	101, …, 131 (7 primes)	137, 139	18,209	14: 20	15: 21
8	127, …, 163 (8 primes)	173, 179	29,177	16: 23	17: 24
9	131, …, 173 (9 primes)	179, 181	31,313	18: 26	19: 27
10	137, …, 181 (10 primes)	191, 193	34,933	20: 29	21: 30
11	163, …, 223 (11 primes)	227, 229	51,067	22: 32	23: 33
12	173, …, 233 (12 primes)	239, 241	56,153	24: 35	25: 36
13	193, …, 263 (13 primes)	269, 271	71,273	26: 38	27: 39
14	223, …, 283 (14 primes)	307, 311	88,013	28: 41	29: 42

Each row was solved exactly by our solver: the "needed" figure is the true minimum for that run, not just a lower bound. We also checked each run directly: u is its only member divisible by two of the primes, and no member is divisible by q_u² or q_v². The runs start at numbers of up to 44 digits; they are in the bundle, with a cover of the stated size for each, which takes one division to check.

One consequence is the one Chen's paper names. His bound g(A, x) ≤ n + β, where β is the cycle rank (the number of independent cycles) of the graph joining each a to its primes, cannot be improved to n + θβ + C for any θ < 1 and any constant C. The family has β = t − 1 and needs exactly n + β integers at every size. The condition q_u² ≥ m + q_u matters. Our first attempt chose primes without it. At t = 9, with primes 127, …, 167 and 173, 179, m = 29,893 is only 36 below 173², so a multiple of 173² landed inside the run and only 25 integers were needed. That failed run is in the bundle.

How it compares. Theorem IV of 1959 gives n + 1. Since g never decreases (add any number up to max A to a hard set; Preil's notes), the 1959 construction also gives g(n) ≥ ℓ(ℓ−1)+1 whenever n ≥ ℓ(ℓ+1)/2. Against both, ⌊3n/2⌋ − 1 ties at n = 4, 5 and 15 and is larger at every other n from 4 to 20. Below 36 it is larger at 26 of the 32 sizes; the 1959 family wins at 21, 28 and 29. The last n where ours is larger is 90; from then on the 1959 family is at least as large, and asymptotically it gives 2n − O(√n). At n = 6, 8, 10 and 12 our values equal Chen's. At n = 7, 9, 11, 13, 14 and 16–20 (and many larger n below 90) they are, as far as we found, the largest lower bounds anyone has recorded.

What this does not do. It does not touch Erdős's question. The upper bound stays at 12n in Lean, or 11n (Chen) and 10n (Wang) refereed by AI instances but not formalised. With the threshold floor of 2, Chen's method as it stands cannot go below about 3n. The exact value of g(4) is open: it is between 5 and 28 (Chen's first theorem gives 28). Everything between the two bounds is open too. The 12n result and its proofs are Chen's, found with GPT-5.6, GPT-6 and Qwen and refereed by Claude instances in his own pipeline. Our part is the replay, the checks above, and the lemma.