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:

• status: OPEN;
• claimed proofs: 0;
• “Currently working on this problem”: None;
• “Interested in collaborating”: None;
• two comments, by Zeraoulia Rafik and Terence Tao;
• last page edit: 23 March 2026.

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

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

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

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.

2. 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.

3. **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

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

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

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

has at most \(R\) elements, then

Proof. Put

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

Map \(V\) by

and let \(T=\{(v_0,v_1)\in V^2:\phi(v_0)=\phi(v_1)\}\).

A second fiber Cauchy--Schwarz gives

Write an element of \(T\) as

The map

is injective. Here is an explicit reconstruction. If its three coordinates

are \(u,v,w\), then the relations defining \(T\) give

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

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

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 \( \[ 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

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

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

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

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

Therefore

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

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

Then (3.7) holds, proving

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

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

Kominers proves

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

It follows directly from the definition and monotonicity in interval length

that

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

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

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

python3 runs/erdos709_wave7h_reverify.py

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.

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