Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


This digest records statement-level content from arXiv:2603.28636v1, submitted 2026-03-30, the copy read for this digest. The edition is identified on the source card.

Definition and theorem statements

For each positive integer mm, let f(m)f(m) be the largest integer rr such that, for every set A={a1<⋯<am}A=\{a_1<\cdots<a_m\} of mm positive integers and every real number xx, there are distinct c1,…,cr∈Ac_1,\ldots,c_r\in A and distinct integers b1,…,brb_1,\ldots,b_r satisfying

x<bi<x+2am,ci∣bi(1≤i≤r).x<b_i<x+2a_m,\qquad c_i\mid b_i\qquad(1\le i\le r).

The paper also writes B=(x,x+2am)∩ZB=(x,x+2a_m)\cap\mathbb Z and lets G(A,x)G(A,x) be the bipartite divisibility graph on AA and BB.

Theorem 2.1 (E650; printed/physical p. 2). For every positive integer mm,

f(m)=min⁡{m,⌈2m⌉}.f(m)=\min\{m,\lceil2\sqrt m\rceil\}.

Remark 2.2 (printed/physical p. 3). For every integer m≥4m\ge4,

f(m)=⌈2m⌉.f(m)=\lceil2\sqrt m\rceil.

Historical comparison (printed/physical p. 1). The paper recalls the Erdős–Surányi lower bound f(m)≥mf(m)\ge\sqrt m and the Erdős–Selfridge estimate f(m2)≤2mf(m^2)\le2m, which gives the general upper bound f(m)≤2⌈m⌉f(m)\le2\lceil\sqrt m\rceil. Thus the earlier general bounds differed by a factor of two.

Theorem 3.1 (printed/physical p. 4). For all positive integers s,ts,t,

f(st)≤s+t.f(st)\le s+t.

The paper's construction (printed/physical pp. 4–5) uses the Chinese Remainder Theorem to produce a set of stst positive integers and an interval of length 2max⁡A2\max A containing at most s+ts+t distinct multiples.

Theorem 4.1 (printed/physical p. 5). For every positive integer mm,

f(m)≥min⁡{m,⌈2m⌉}.f(m)\ge\min\{m,\lceil2\sqrt m\rceil\}.

The paper's lower-bound proof applies a generalization of Hall's theorem (Lemma 2.3, p. 3, the König–Ore formula) to G(A,x)G(A,x). Together Theorems 3.1 and 4.1 give Theorem 2.1.

Interval-length range (printed/physical pp. 1--2 and 5). Although the displayed definition of f(m)f(m) uses intervals of length 2am2a_m, the introduction says that the same results remain valid when 2 is replaced by any real multiplier cc with 2≤c<32\le c<3. More precisely, Remark 3.3 says that, for every ε∈(0,1)\varepsilon\in(0,1), the upper-bound construction still works with an interval of length (3−ε)max⁡A(3-\varepsilon)\max A once MM is chosen larger than ε−1(3−ε)(s+tD)\varepsilon^{-1}(3-\varepsilon)(s+tD). This records the source's parameter extension; it is not a new local proof.

Verification layers

Formal source. The paper cites Wouter van Doorn's ErdosProblem650.lean. Its Section 5 records Lean version leanprover/lean4:v4.28.0 and Mathlib commit 8f9d9cff6bd728b17a24e163c9402775d9e6a365. No local Lean environment or build was used.

Reported verification. The paper reports (Sections 1.1 and 5) that an initial draft produced by a large language model found the main strategy but contained a gap in the Case 2 injection, and that an automated theorem-proving system supplied a working variation and a complete Lean formalization. It says the final exposition and proofs are human-written. These are author-reported workflow claims, recorded without model or system names.

Local verification. The copy read for this digest is the arXiv v1 PDF, submitted 2026-03-30. All eight page images were read for the definition, historical comparison, interval-range and CRT statements, Theorems 2.1, 3.1 and 4.1, and the formalization account. This check records source statements and provenance only. Read status: claims checked for the definition of f(m)f(m), Theorem 2.1, Remark 2.2, Lemma 2.3, Theorem 3.1, Remark 3.3 and Theorem 4.1, read clause by clause on the page images; the proofs of Sections 3 and 4 were read but not independently checked. Each result has its own page, linked from the source card.

Problem scope

Theorem 2.1 directly addresses E650. E860 is adjacent context only: the paper does not mention it, and E860's h(n)h(n), the interval length needed to match the primes up to nn to distinct multiples, is a different function from f(m)f(m).