ERDŐS/DAILY ▸

← back to the ledger

ERDőS #709 · PROVED

Erdős problem #709 — wave 7h

Accessed and checked on 2026-07-27 (UTC). This report was produced with AI assistance (Codex / GPT-5.6); all finite claims below were recomputed by the standalone standard-library checker runs/erdos709_wave7h_reverify.py.

0. Mandatory live-page audit

I fetched the Cloudflare-protected live page and its discussion thread through the Bright Data browser, not through datacenter curl.

Live state:

Thus none of the mandated stop conditions applies.

The following is the verbatim statement from the page's LaTeX source:

Let \(f(n)\) be minimal such that, for any \(A=\{a_1,\ldots,a_n\}\subseteq [2,\infty)\cap\mathbb{N}\) of size \(n\), in any interval \(I\) of \(f(n)\max(A)\) consecutive integers there exist distinct \(x_1,\ldots,x_n\in I\) such that \(a_i\mid x_i\).

Obtain good bounds for \(f(n)\), or even an asymptotic formula.

The page attributes the problem to Erdős--Surányi [ErSu59] and records

\[ (\log n)^c\ll f(n)\ll n^{1/2} \]

for some \(c>0\), together with the newer displayed lower bound

\[ \frac{\log n}{\log\log n}\ll f(n) \]

obtained from van Doorn's result for problem #711. It also points to problem #708.

The first forum comment gives precisely that van-Doorn transfer, using the consecutive moduli, and discloses use of ChatGPT 5.4. Tao's reply corrects the size-\(n\) family to \(A=\{2,3,\ldots,n+1\}\), records the old exponent

\[ c=1-\frac{1+\log\log 2}{\log 2}=0.0860713320\ldots, \]

and notes that Erdős--Pomerance [ErPo80] already gives the intermediate \(\sqrt{\log n/\log\log n}\) lower bound. The comments contain no solution claim and no worker marker.

Authoritative page: <https://www.erdosproblems.com/709>. Discussion: <https://www.erdosproblems.com/forum/thread/709>.

1. Results obtained

Write \(f_{709}\) when it is useful to distinguish the function on the live page from similarly named functions in the literature.

  1. Improved upper exponent — (a) elementary-rigorous. For every

\(n\geq 1\),

\[ \boxed{\quad f_{709}(n)\leq 7\left\lceil n^{3/7}\right\rceil \leq 14n^{3/7}. \quad} \]

The proof below is self-contained: Hall's theorem, two finite Cauchy--Schwarz inequalities, and an explicit injection. This improves the page's \(O(\sqrt n)\) exponent.

  1. Improved lower bound — (b) rigorous modulo a named theorem. Theorem

1.1 of Kominers, arXiv:2607.10431v1 (submitted 11 July 2026, after the live page's last edit), implies

\[ \boxed{\quad \liminf_{n\to\infty}\frac{f_{709}(n)}{\log n}\geq\frac1e. \quad} \]

This removes the \(\log\log n\) denominator from the page's current lower bound. The only non-elementary input is Kominers' theorem, which in turn uses Hildebrand--Tenenbaum local estimates for smooth numbers.

  1. **Concrete Hall certificate — (d) computational-only for the counts,

with an elementary Hall implication.** Let

\[ A=\{2,3,\ldots,1{,}000{,}000\} \]

and

\[ I=(28{,}920{,}105,\ 33{,}071{,}408]. \]

This interval has \(4{,}151{,}303\) consecutive integers. The explicitly defined subfamily

\[ S=\{\,i:2\leq i\leq10^6,\ i\cdot126>33{,}071{,}408,\ P^+(i)\leq126\,\} \]

has 52,228 elements, while its actual neighborhood in \(I\),

\[ \Gamma_I(S)=\{x\in I:\text{some }i\in S\text{ divides }x\}, \]

has only 52,227 elements. Hence Hall fails and

\[ \boxed{\quad f_{709}(999{,}999)> \frac{4{,}151{,}303}{1{,}000{,}000}=4.151303. \quad} \]

Under the natural integer-scale convention this says \(f_{709}(999999)\geq5\).

Combining the two asymptotic results gives the currently verified sandwich

\[ \left(\frac1e-o(1)\right)\log n \ \leq\ f_{709}(n)\ \leq 7\left\lceil n^{3/7}\right\rceil. \]

This is substantial progress but not an asymptotic formula, so the problem remains open.

2. Hall reformulation

Fix a finite modulus family \(A\), an integer interval \(I\), and put

\[ \Gamma_I(S)=\{x\in I:\exists a\in S,\ a\mid x\} \qquad(S\subseteq A). \]

The desired distinct divisible representatives are exactly a matching that saturates the \(A\)-side of the divisibility bipartite graph. Hall's theorem therefore says that they exist if and only if

\[ |\Gamma_I(S)|\geq |S|\qquad\text{for every }S\subseteq A. \tag{2.1} \]

This equivalence is (a) elementary-rigorous and will be used in both directions.

3. The \(3/7\) upper bound

3.1 A finite four-projection lemma

Lemma. Let \(G\) be finite and let \(a,b:G\to\mathbb Z\), with \(g\mapsto a(g)-b(g)\) injective. If each of the four images

\[ a(G),\qquad b(G),\qquad (a+b)(G),\qquad (a+2b)(G) \]

has at most \(R\) elements, then

\[ |G|^4\leq R^7. \tag{3.1} \]

Proof. Put

\[ V=\{(x,y)\in G^2:a(x)=a(y)\}. \]

Cauchy--Schwarz over the fibers of \(a\) gives

\[ |G|^2\leq |a(G)|\,|V|\leq R|V|. \tag{3.2} \]

Map \(V\) by

\[ \phi(x,y)=(a(x)+2b(x),\,b(y)), \]

and let \(T=\{(v_0,v_1)\in V^2:\phi(v_0)=\phi(v_1)\}\). A second fiber Cauchy--Schwarz gives

\[ |V|^2\leq |(a+2b)(G)|\,|b(G)|\,|T| \leq R^2|T|. \tag{3.3} \]

Write an element of \(T\) as

\[ t=((x_0,y_0),(x_1,y_1)). \]

The map

\[ t\longmapsto \bigl(a(x_0)+b(x_0),\ a(y_0)+b(y_0),\ b(x_1)\bigr) \tag{3.4} \]

is injective. Here is an explicit reconstruction. If its three coordinates are \(u,v,w\), then the relations defining \(T\) give

\[ (a-b)(y_1)=2u-v-2w. \]

Injectivity of \(a-b\) determines \(y_1\). Then \(b(y_0)=b(y_1)\); \(v=a(y_0)+b(y_0)\) determines \((a-b)(y_0)\), hence \(y_0\). Now \(a(x_0)=a(y_0)\) and \(u=a(x_0)+b(x_0)\) determine \((a-b)(x_0)\), hence \(x_0\). Finally \(a(x_0)+2b(x_0)=a(x_1)+2w\) determines \((a-b)(x_1)\), hence \(x_1\). Thus (3.4) is injective and

\[ |T|\leq |(a+b)(G)|^2|b(G)|\leq R^3. \tag{3.5} \]

Squaring (3.2) and using (3.3)--(3.5) yields

\[ |G|^4\leq R^2|V|^2\leq R^4|T|\leq R^7. \]

This proves the lemma. \(\square\)

Every step above is finite and exact; this is classification (a), not an appeal to a conjectural sum-product estimate.

3.2 One block

Let \(M=\max A\), let \(S\subseteq A\), and consider any block \(J\) of \(7M\) consecutive integers. For each \(d\in S\), let \(p_d\) be its first multiple in \(J\). Its offset from the start of \(J\) is \(<d\), so

\[ p_d,\quad p_d+3d,\quad p_d+4d,\quad p_d+6d \]

all lie in \(J\), and all belong to \(B=\Gamma_J(S)\).

Apply the lemma with

\[ a(d)=p_d,\qquad b(d)=p_d+6d. \]

Both \(a(S)\) and \(b(S)\) lie in \(B\). Moreover

\[ a(d)+b(d)=2(p_d+3d),\qquad a(d)+2b(d)=3(p_d+4d). \]

Multiplication by 2 or 3 is injective on \(\mathbb Z\), so both of these image sizes are at most \(|B|\). Finally \(a(d)-b(d)=-6d\) is injective because the moduli in \(S\) are distinct. Consequently

\[ |S|^4\leq |\Gamma_J(S)|^7. \tag{3.6} \]

3.3 Aggregate disjoint blocks

Take \(k\) consecutive, disjoint \(7M\)-blocks. For a fixed \(S\subseteq A\), write \(m=|S|\) and \(r_j=|\Gamma_{J_j}(S)|\). If

\[ n^3\leq k^7, \tag{3.7} \]

then \(m^3\leq k^7\), while (3.6) gives \(m^4\leq r_j^7\). Therefore

\[ m^7\leq (kr_j)^7,\qquad\text{so }m\leq kr_j \]

for every \(j\). Summing and dividing by \(k>0\) gives

\[ m\leq\sum_{j=1}^k r_j. \]

The blocks are disjoint, so the sum is the size of their disjoint neighborhood union, which is contained in the global neighborhood. Thus (2.1) holds for every \(S\), and the whole interval of length \(7kM\) has the required matching.

Choose

\[ k=\left\lceil n^{3/7}\right\rceil. \]

Then (3.7) holds, proving

\[ f_{709}(n)\leq7\left\lceil n^{3/7}\right\rceil. \]

Since \(\lceil x\rceil\leq x+1\leq2x\) for \(x\geq1\), the displayed \(14n^{3/7}\) bound follows.

3.4 Provenance and independent audit

A web search found a public Star Fleet Math bundle dated 14 July 2026 that states the slightly weaker exact rounding

\[ 7\bigl(\lfloor(n^3)^{1/7}\rfloor+1\bigr) \]

and contains a Lean 4 formalization of the same four-projection/block proof: <https://www.starfleetmath.com/>. The public source archive was downloaded from the bundle link on that page; its SHA-256 is

003bcc5f49c21bfb54ca5a7b450842124191414796a25c66d85019aec625ba9b

I checked the canonical definition against the live statement, inspected the entire proof chain used above, and found no sorry, admit, custom axiom, native_decide, unsafe, or extern in the Lean sources. The archive records the axiom closure as exactly [propext, Classical.choice, Quot.sound].

I did not run its full approximately 8,000-job Mathlib rebuild because the bundle estimates about 20 minutes and the task forbids heavy computation. That omission does not affect the classification of the result here: the finite argument in §§3.1--3.3 was reconstructed and checked independently. The rounding to \(7\lceil n^{3/7}\rceil\) is a small exact sharpening of the bundle when \(n^3\) is a seventh power. I found no journal or arXiv paper stating this #709 upper bound, so I make no priority or publication claim.

4. Transfer of Kominers' lower bound

For \(N,m\geq1\), let \(h(N,m)\) be the least \(H\) such that \((m,m+H]\) contains pairwise distinct multiples of \(1,2,\ldots,N\), and let

\[ H(N)=\max_m h(N,m). \]

Kominers proves

\[ \liminf_{N\to\infty} \frac{H(N)-h(N,N)}{N\log N}\geq\frac1e. \tag{4.1} \]

The Erdős--Pomerance upper estimate \(h(N,N)=o(N\log N)\) therefore makes (4.1) equivalent to the following: for every fixed \(C<1/e\) and all sufficiently large \(N\), some interval of \(\lfloor C N\log N\rfloor\) consecutive integers has no system of distinct multiples of \(1,\ldots,N\).

For large \(N\), this interval has at least \(N\) elements. If it had a matching for \(2,3,\ldots,N\), those \(N-1\) representatives would leave an unused interval element; assigning that unused element to modulus \(1\) would extend the matching to \(1,\ldots,N\), a contradiction. Hence the same interval fails for

\[ A_N=\{2,3,\ldots,N\}, \qquad |A_N|=N-1,\quad \max A_N=N. \]

It follows directly from the definition and monotonicity in interval length that

\[ f_{709}(N-1)> \frac{\lfloor C N\log N\rfloor}{N}. \]

Letting \(N\to\infty\), then \(C\uparrow1/e\), proves

\[ \liminf_{n\to\infty}\frac{f_{709}(n)}{\log n}\geq\frac1e. \]

The transfer is (a) elementary-rigorous; (4.1) is the sole (b) rigorous-modulo-named-theorem input.

Primary source: S. D. Kominers, “Long Intervals Without Distinct Multiples of the First \(n\) Positive Integers,” arXiv:2607.10431v1 (2026), <https://arxiv.org/abs/2607.10431>. The title, author, identifier, submission date, theorem, and \(1/e\) constant were checked in the paper itself. The paper discusses problems #710 and #711 but does not mention #709, which explains why this immediate transfer is absent from the March live page.

5. The finite certificate and checker

The search uses the elementary smooth-index obstruction. For fixed \((N,y,E)\), take

\[ S=\{i:E/y<i\leq N,\ P^+(i)\leq y\}. \]

Every multiple \(iq\leq E\) of \(i\in S\) has \(q<y\), so all its prime factors are at most \(y\). The search compares the exact eligible-index count with exact smooth-target counts, chooses the longest candidate interval for fixed \((N,y)\), and then moves the left endpoint farther left until the actual divisibility neighborhood has exactly \(|S|-1\) points.

For \(N=10^6,y=126\), it found the certificate in §1. The final verification does not rely on the smooth-target upper bound: it constructs every multiple of every \(i\in S\) in the interval, unions them as integers, and independently marks the same union in a dense bit vector. The stable hashes are

SHA256(S)    = d1014f01ae5bba487cf66fffff73091fb72c37f08028066847b537248a18c529
SHA256(Gamma)= ab39ba55f9d77fec7299f9cd1a1df4a65c818ba9bbdc1de4cc2f1d5ff534ee0b

Reverification:

python3 runs/erdos709_wave7h_reverify.py

Observed output:

UPPER-BOUND ARITHMETIC: exact 7-block, seventh-root, 14*n^(3/7), and aggregation checks passed.
FOUR-PROJECTION SANITY: 23563 exhaustive small instances passed.
FINITE HALL CERTIFICATE: A={2,...,1000000} (size 999999), I=(28920105,33071408] (length 4151303), |S|=52228, |N(S)|=52227.
SHA256(S)=d1014f01ae5bba487cf66fffff73091fb72c37f08028066847b537248a18c529
SHA256(N(S))=ab39ba55f9d77fec7299f9cd1a1df4a65c818ba9bbdc1de4cc2f1d5ff534ee0b
Therefore f(999999) > 4151303/1000000 = 4.151303000000.

Measured default-check cost on this VM: 1.47 seconds and 31 MB maximum RSS. The optional exact search

python3 runs/erdos709_wave7h_reverify.py --search --N 1000000 --y 126

took 8.16 seconds and 241 MB maximum RSS. No randomized or floating-point decision is used. The checker also exhausts 23,563 small instances of the four-projection inequality and checks all rounding/aggregation inequalities with exact integer powers; those tests are sanity checks, while §3 is the uniform proof.

6. Literature audit

The following primary sources were located and checked:

zu einer Aufgabe eines mathematischen Wettbewerbs,” Matematikai Lapok 10 (1959), 39--48. The original scan states this matching problem and proves the polylogarithmic lower and \(O(\sqrt n)\) upper bounds: <https://users.renyi.hu/~p_erdos/1959-07.pdf>.

distinct multiples in another interval,” Indagationes Mathematicae 83(2) (1980), 147--161. (The first forum comment says 147--151; the paper itself runs through page 161.) Its scan is <https://users.renyi.hu/~p_erdos/1980-13.pdf>.

of the first \(n\) positive integers,” INTEGERS 26 (2026), #A7. Theorem 1 gives the \(0.36N\log N/\log\log N\) obstruction used on the live page: <https://math.colgate.edu/~integers/aa7/aa7.pdf>.

source that raises that obstruction to \((1/e-o(1))N\log N\).

Hardy--Ramanujan Journal 15 (1992), 34--50, DOI <https://doi.org/10.46298/hrj.1992.125>.

Exact-title, exact-statement, citation, arXiv, and web searches did not locate another conventional publication improving #709 itself. That is a reported search miss, not a claim that none exists. The July Star Fleet artifact is described separately in §3.4 because it is a public proof bundle rather than a journal/arXiv paper.

7. What remains

The order gap is still large:

\[ \log n\quad\text{versus}\quad n^{3/7}. \]

The exact upper-bound bottleneck isolated by the proof is now concrete. For the four selected points \(0,3,4,6\) of each distinct-step progression, the universal projection estimate is

\[ \#\{\text{progressions}\}\leq |B|^{7/4}. \]

A stronger fixed-slice estimate

\[ \#\{\text{distinct-step progressions}\}\leq |B|^{1/\alpha} \quad\text{with }\alpha>4/7 \]

would, by the identical block argument, improve the exponent from \(3/7\) to \(1-\alpha\). Reaching a polylogarithmic upper bound would require a family of slice/structure estimates with \(\alpha\to1\), or a different global argument. That is the precise missing upper lemma; merely iterating the present four-projection estimate cannot do it.

On the lower side, the consecutive family \(\{2,\ldots,N\}\) now supplies the \((1/e-o(1))\log n\) obstruction. Determining whether arbitrary modulus families produce substantially worse Hall violators requires a structure theorem for subfamilies whose multiples overlap heavily in every long interval. Smooth families are one mechanism, but neither the sources nor the computation prove they are extremal.

An exact global finite computation also does not close this gap. Even for a fixed modulus family, the starting point is periodic modulo its lcm, already exponential for \(\{1,\ldots,N\}\); for arbitrary \(A\), \(\max A\) is unbounded. A complete small-\(n\) computation therefore first needs a theorem bounding \(\max A\) or classifying minimal Hall obstructions. Brute force over the unbounded moduli or the full lcm period is not a legitimate finite verification.

PROVED: \((1/e-o(1))\log n\le f_{709}(n)\le7\lceil n^{3/7}\rceil\), with a direct checked Hall certificate \(f_{709}(999999)>4.151303\); the asymptotic order remains open.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger