Erdoes #1212 - working report - Erdős Problem a Day

Erdős problem #1212 — live-page audit and a primorial drift bound

Access date: 2026-07-27 (UTC).

0. Mandatory live-page gate

I fetched the rendered live problem page,

its LaTeX view, and its discussion thread through the Bright Data browser path.

The observations below are therefore from the live page, not the stale tracker

YAML.

The exact current statement, copied verbatim from the page's LaTeX view, is:

> Let $G$ be the graph with vertex set those pairs $(x,y)\in \mathbb{N}^2$ with

> $\mathrm{gcd}(x,y)=1$, in which we join two vertices if the differ in only one

> coordinate, and there by $\pm 1$.

> Is there a path going to infinity on $G$, say $P$, such that for all

> $(x,y)\in P$ both $\min(x,y)>1$ and at least one of $x$ or $y$ is composite?

Live status and collision markers:

Status: OPEN.
Claimed proofs: 0.
Currently working on this problem: None.
Interested in collaborating: None.
“I am working on formalising the results”: None. The difficulty,

tractability, and formalisability-result markers are also None.

Likes this problem: Dogmachine.
The page says it was last edited 08 April 2026.

Thus the requested stop condition did not fire.

The page's listed background says:

Herzog and Stewart studied visible lattice points and, according to Erdős,

proved uniqueness of the unrestricted infinite component. The page owner

could not locate this result in their 1971 paper.

For the weaker problem without the prime-pair prohibition, Stewart joined

successive prime-pair vertices by horizontal and vertical legs; the page

checks these legs using $p_{k+2}<2p_k$ for $k\geq4$.

The page asks in addition about a monotone path and bounded run lengths

between direction changes.

There are two live comments. The first only reports typographical errors. The

second, by ephraimduncan on 21 July 2026, links a Lean repository and claims:

a $D!$-wall drift obstruction; arbitrary finite “elevator” paths; twin-prime

isolated vertices; and large finite computational components. It explicitly

says the problem remains open. I independently prove a strictly sharper wall

bound below and independently recompute its small examples; I do not use the

comment as an authority.

1. Claim labels

Every mathematical claim below is marked as requested:

(a) elementary-rigorous — a complete elementary proof is supplied.
(b) rigorous-modulo-named-theorem — the precise external theorem is named.
(c) plausible/structural-unverified — heuristic only.
(d) computational-only — exactly reproduced by the standalone checker,

but not promoted to a theorem.

Source-status and bibliographic observations are labelled source-verified

rather than being mathematical claims.

2. Primary-source literature audit

1. Erdős 1980 (source-verified). I inspected page 114 of the Rényi archive

scan of P. Erdős, [*A survey of problems in combinatorial number

theory](https://www.renyi.hu/~p_erdos/1980-03.pdf), Annals of Discrete

Mathematics* 6 (1980), 89–115. It contains the weaker Stewart story and then

asks for a path avoiding prime-prime points and points having a coordinate

1. It supplies no proof or partial result for the strengthened question.

2. **Herzog–Stewart 1971 (source-verified bibliographically; content miss

reported honestly).** The article exists as F. Herzog and B. M. Stewart,

[*Patterns of Visible and Nonvisible Lattice

Points](https://doi.org/10.2307/2317753), Amer. Math. Monthly* 78 (1971),

487–496. JSTOR exposed only the bibliographic preview in this run, not the

article text. I therefore do not attribute a connectivity theorem to that

paper. This agrees with the live page's explicit caution.

3. Vardi 1999 (source-verified). I inspected I. Vardi,

[*Deterministic

Percolation*](https://www.lix.polytechnique.fr/Labo/Ilan.Vardi/deterministic_percolation.pdf),

Commun. Math. Phys. 207 (1999), 43–66. Proposition 3.1 proves that the

unrestricted graph

\[ R=\{(m,n)\in\mathbb Z^2:\gcd(m,n)=1\} \]

has one infinite component; Theorems 3.2–3.4 concern its density. The

isolated residue-class example near $(4,15)\bmod30$ is also for that

unrestricted graph. None of these results removes coordinate-1 vertices and

all prime-prime vertices, so none answers #1212.

4. Local limits and random coprime percolation (source-verified).

S. Martineau, arXiv:1804.06486, proves a

local-limit description of translated coprime colourings. S. Le Fourn,

M. Liu, and S. Martineau,

arXiv:2509.08452, Theorem 1.1, prove that

the random local-limit colouring on the ordinary square lattice almost

surely has one infinite white cluster and no infinite black cluster.

(a) This does not imply that the one fixed composite-protected graph in

#1212 has an infinite component: local convergence controls every fixed

finite window, whereas existence of an infinite component is not a local

property. Graphs made of larger and larger disjoint finite boxes give the

standard logical counterexample to such an inference.

5. 2026 formal work (source-verified). Google DeepMind

formal-conjectures [PR

#4218](https://github.com/google-deepmind/formal-conjectures/pull/4218) was

merged on 24 June 2026 (the discussion comment saying “closed without

merging” is stale). The merged file leaves the open statement under

answer(sorry) and proves supporting leg/roughness lemmas. Its PR description

explicitly identifies an unproved every-interval hypothesis for rough

composites. The separate

ephraimduncan/erdos-1212

repository proves the $D!$-drift result reported in the live comment and

expressly does not claim a solution.

6. Short-interval almost primes (source-verified).

K. Matomäki, arXiv:2012.11565,

Theorem 1.1, finds $\gg h$ $P_2$-numbers with every prime factor

$>X^{1/8}$ in almost every interval of length $h\log X$. A $P_2$

number may itself be prime, so this does not supply the required composite

anchors.

K. Matomäki and J. Teräväinen,

arXiv:2207.05038, Theorem 1.1, find

$\gg(\log x)^{1.1}$ products $p_1p_2$ in almost every interval

$(x,x+(\log x)^{2.1}]$, with

\((\log x)^{1.09}

Exact-title, exact-statement, “visible lattice connectivity,” “rough

composite,” and primorial-wall searches found no primary source that settles

the composite-protected deterministic question. In particular, I found no

claimed proof beyond the zero claims shown on the live page.

3. New elementary result: the exact primorial wall

Write

\[ \Delta(x,y)=|y-x|,\qquad Q(D)=\prod_{\substack{p\leq D\\p\ {\rm prime}}}p \]

(the empty product is $1$). The live comment uses $D!$. Squarefree

$Q(D)$ is enough, and it gives the exact least modulus for a universal

one-column wall.

Theorem 1 — primorial strengthening of the bounded-strip obstruction (a)

Let $v_n=(x_n,y_n)$ be any finite or infinite unit-step walk through pairs

with

\[ x_n,y_n>1,\qquad \gcd(x_n,y_n)=1. \]

The compositeness condition is not needed. Suppose

$\Delta(x_n,y_n)\leq D$ throughout, where $D\geq1$, and put

$s_0=\min(x_0,y_0)$. Define

\[ M=Q(D)\left\lceil\frac{s_0}{Q(D)}\right\rceil . \]

Then, for every $n$,

\[ \min(x_n,y_n)\leq M,\qquad \max(x_n,y_n)\leq M+D,\qquad x_n+y_n\leq 2M+D. \tag{1} \]

In particular,

\[ x_n+y_n\leq 2s_0+2Q(D)-2+D. \tag{2} \]

Proof

(a) A valid walk cannot touch the diagonal: at $(t,t)$, with $t>1$,

the gcd is $t$. A unit step changes the signed offset $y-x$ by $1$ or

$-1$. Therefore its sign cannot change without first being zero. The same

coordinate remains the smaller one for the whole walk.

By symmetry assume \(x_n

multiple of every prime at most $D$ and satisfies $M\geq x_0$. Suppose the

walk ever reaches a point with $x>M$, and take the first such step. It must

be an east step

\[ (M,M+d)\longrightarrow(M+1,M+d) \]

with $1\leq d\leq D$.

If $d=1$, the new point is $(M+1,M+1)$, which is not a vertex.
If $d\geq2$, choose a prime $p\mid d$. Then $p\leq D$, hence

$p\mid Q(D)\mid M$, and also $p\mid M+d$. Thus

$\gcd(M,M+d)>1$, so the old point was not a vertex.

Both cases are contradictions. Hence $x_n\leq M$, and

$y_n=x_n+(y_n-x_n)\leq M+D$. This proves (1). The least multiple of $Q(D)$

at or to the right of $s_0$ is at most $s_0+Q(D)-1$, which gives (2).

The case \(y_n

Exactness of the modulus (a)

A column $m$ blocks every possible offset $d=2,\ldots,D$ by

non-coprimality exactly when

\[ \gcd(m,d)>1\quad(2\leq d\leq D). \tag{3} \]

Condition (3) holds if and only if every prime $p\leq D$ divides $m$:

necessity follows by taking $d=p$, and sufficiency follows by taking any

prime divisor of $d$. Consequently the universal wall columns are precisely

the multiples of $Q(D)$. Thus $Q(D)$, not $D!$, is the least possible

modulus for this one-column argument. This is an exactness statement about the

wall mechanism, not a claim that every conceivable global obstruction must be

a single column.

Quantitative record drift (a), and its asymptotic form (b)

For a prefix $0\leq n\leq N$, set

\[ D_N=\max_{0\leq n\leq N}|y_n-x_n|,\qquad R_N=\max_{0\leq n\leq N}(x_n+y_n). \]

The finite version of the proof gives the exact inequality

\[ R_N\leq 2Q(D_N)\left\lceil\frac{s_0}{Q(D_N)}\right\rceil+D_N. \tag{4} \]

This strengthens “the offset is unbounded” to an explicit rate for record

offsets.

(b, prime number theorem). Since

\[ \log Q(D)=\sum_{p\leq D}\log p=(1+o(1))D, \]

equation (4) implies, along every path with $R_N\to\infty$,

\[ D_N\geq(1-o(1))\log R_N, \tag{5} \]

where the logarithm is natural. This is a record-offset statement; it does not

assert that every individual far-away vertex has logarithmic offset.

For comparison, with $s_0=1000$:

| $D$ | $Q(D)$ | new exact $2M+D$ | posted $2D!(s_0+1)+D$ |

|---:|---:|---:|---:|

| 5 | 30 | 2,045 | 240,245 |

| 11 | 2,310 | 4,631 | 79,913,433,611 |

| 13 | 30,030 | 60,073 | 12,466,495,641,613 |

| 23 | 223,092,870 | 446,185,763 | 51,755,737,511,247,723,233,280,023 |

All entries are (d) exact-integer recomputations by the checker.

4. Composite-anchor reduction and what current sieve theorems give

For a composite $a$, let $P^-(a)$ be its least prime factor.

Lemma 2 — sufficient anchor sequence (a)

Suppose there is a strictly increasing infinite sequence of composites

\(a_0 \[ a_{i+2}-a_i< \min\bigl(P^-(a_i),P^-(a_{i+2})\bigr) \tag{6} \]

for every $i$. Then #1212 has a positive answer.

Indeed, concatenate the L-shaped legs

\[ (a_i,a_{i+1}) \to(a_i,a_{i+1}+1)\to\cdots\to(a_i,a_{i+2}) \to(a_i+1,a_{i+2})\to\cdots\to(a_{i+1},a_{i+2}). \tag{7} \]

(a) Every vertex in the vertical leg is coprime because a common prime

would divide a positive difference \(

argument applies to the horizontal leg and $a_{i+2}$. One fixed coordinate

on every leg is composite, both coordinates exceed $1$, the path is

monotone, and strict increase of the anchors makes it go to infinity.

This is only a sufficient reduction; a solution need not have this shape.

A rigorous finite consequence of Matomäki–Teräväinen (b)

(b, Matomäki–Teräväinen Theorem 1.1). In a good interval

$(x,x+(\log x)^{2.1}]$, partition the interval into cells of length at most

$\tfrac12(\log x)^{1.09}$. There are

$O((\log x)^{1.01})$ cells but

$\gg(\log x)^{1.1}$ exact semiprimes of the theorem. Hence one cell contains

\[ \gg(\log x)^{0.09} \]

of them. For sufficiently large $x$, their displayed factor $p_1$ is

their least prime factor and exceeds $(\log x)^{1.09}$. Sorting the

semiprimes in that one cell therefore gives a finite anchor sequence satisfying

(6). Consequently, for almost all large $x$, the qualifying graph contains a

monotone composite-anchor staircase with

$\gg(\log x)^{0.09}$ anchors inside a square of side

$\tfrac12(\log x)^{1.09}$.

This does not furnish one infinite sequence. The dense cells may occur at

unrelated locations, and the theorem allows exceptional intervals. Passing

from arbitrarily long finite paths at varying locations to one fixed infinite

component is exactly the missing compactness/uniformity step.

Explicit finite certificate (d)

The checker embeds 52 increasing composite anchors from $199{,}973$ through

$200{,}549$, verifies (6) by fresh trial division, constructs (7), and checks

every vertex and edge. The result is a monotone path with:

1,133 vertices and 1,132 edges;
99 direction changes;
start $(199973,199987)$ and end $(200543,200549)$;
maximum diagonal offset 90.

This is an explicit, independently checkable finite certificate, not an

infinite construction and not an optimality claim.

5. Exact computations and reproduction

Standalone verifier:

runs/erdos1212_wave6y_reverify.py.

Run from the repository root:

python3 runs/erdos1212_wave6y_reverify.py

It uses only the Python standard library. It independently implements Euclid's

algorithm, trial-division primality and least-prime-factor tests. It then:

1. brute-forces the least wall modulus for every $1\leq D\leq13$;

2. checks every wall offset for $D\leq60$ and the first five wall multiples;

3. exhausts the unrestricted qualifying components of $(3,4)$ and

$(9,10)$, obtaining respectively

$\{(3,4)\}$ and

$\{(8,11),(9,10),(9,11),(10,11)\}$;

4. exhausts induced bounded-strip components with a direct no-exit check;

5. checks the 1,133-vertex staircase; and

6. recomputes all numerical tables.

Representative exact strip data (d) are:

|---|---:|---:|---:|---:|---:|---:|

| (49,50) | 4 | 6 | 54 | 9 | 52 | 4 |

| (49,50) | 13 | 30,030 | 30,030 | 20 | 52 | 11 |

| (121,122) | 6 | 30 | 150 | 21 | 126 | 6 |

| (121,122) | 13 | 30,030 | 30,030 | 60 | 126 | 13 |

| (1000,1001) | 6 | 30 | 1,020 | 48 | 1,008 | 6 |

| (1000,1001) | 13 | 30,030 | 30,030 | 120 | 1,008 | 13 |

For $s_0=3$, inversion of the exact bound (4) gives (d):

| prefix reaches $R_N\geq$ | required record offset $D_N\geq$ |

|---:|---:|

| $10^3$ | 11 |

| $10^6$ | 17 |

| $10^9$ | 29 |

| $10^{12}$ | 37 |

| $10^{18}$ | 47 |

| $10^{30}$ | 79 |

The final executed output was ALL CHECKS PASSED; py_compile also succeeded.

6. Exact remaining wall

The original question is not closed.

(a) The primorial theorem proves that any solution must leave every

bounded diagonal strip, quantitatively with logarithmic record drift.

(b) Current almost-prime theorems produce arbitrarily large finite

clusters of anchors but do not control every interval or connect the clusters

into one infinite sequence.

(c) The large components seen in the live comment and the random-limit

percolation theorem make a positive answer plausible, but neither is a

deterministic infinite-path certificate.

For the composite-anchor route, the exact missing lemma is:

> Prove the existence of one infinite increasing composite sequence satisfying

> (6), or prove a strong enough every-interval maximum-gap theorem for rough

> composites to construct such a sequence.

Matomäki's $P_2$ theorem has the needed roughness but not guaranteed

compositeness; Matomäki–Teräväinen guarantees compositeness but only in

almost-all windows whose full length is much larger than the certified least

factor. That mismatch is the precise analytic obstruction.

No larger computation can supply the missing uniform infinitude step. As a

scale warning, explicitly exploring a full $10^6\times10^6$ box would touch

$10^{12}$ lattice positions: a dense one-byte bitmap alone is about 1 TB,

while practical BFS state can require several to tens of terabytes. At a

sustained $10^6$–$10^7$ vertex checks per core-second, even one pass costs

roughly 28–278 core-hours, before queue and edge overhead. It would still

certify only a finite box, so I did not run it.

PARTIAL: proved an elementary primorial-strengthened bounded-strip theorem and logarithmic record-drift bound, derived long finite monotone staircases from a named almost-prime theorem, and supplied an exact standalone checker; the infinite path remains open.

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