---

Claim. Read Problem 450 with the bound required for every translate $x$: call a length $y$ sufficient for $\epsilon$ and $n$ when every interval $(x,x+y)$ of integers, for every $x\ge0$, contains at most $\epsilon y$ integers with a divisor in $(n,2n)$, and let $y(\epsilon,n)$ be the least $y_0$ such that every $y\ge y_0$ is sufficient. The claim is that for every fixed $0<\epsilon<1$ the order of $y(\epsilon,n)$ is linear in $n$: $y(\epsilon,n)=\Theta_\epsilon(n)$. For $\epsilon\ge1$ the question is trivial, since an open window of length $y$ holds at most $y-1<\epsilon y$ integers, so every length is sufficient. The upper bound is explicit. Choose a finite set $S_\epsilon$ of primes, all at least $5$, with $\sum_{p\in S_\epsilon}1/p>152/\epsilon$, and put $Q_\epsilon=\prod_{p\in S_\epsilon}p^2$; then $y=n(Q_\epsilon+2)$ is sufficient for all large $n$. For the lower bound, for every fixed $0<\epsilon<1$ and all large $n$ the length $y=n$ is not sufficient, so any sufficient threshold exceeds $n$ eventually. The write-up is the solution page on Star Fleet Math linked above.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim the optimal order is linear: an explicit $y=n(Q_\epsilon+2)$ works for every translate $x$, and no $o(n)$ length works for any fixed $0<\epsilon<1$, so $y(\epsilon,n)=\Theta_\epsilon(n)$. Proved in Lean 4 / Mathlib (theorem turanLinearAnswer_isSufficientScale plus a matching lower-bound theorem), standard axioms only, no sorry. Idea: the bound must hold for every $x$, which defeats global density arguments (just past a factorial translate, a length-$n$ interval has $n-1$ integers with such a divisor; that is also the lower obstruction). Fix a finite set $S$ of primes and let $U(m)=|{p\in S: p\mid m}|$. The inequality $U(d)+U(k)\le W(dk)$, where $W$ also counts square factors, forces every bad $m=dk$ into one of three rare classes, each periodic mod $\prod_{p\in S}p^2$ and controlled on every interval by Chebyshev and Markov bounds. Notes: Verify: run the included checker (rejects sorry/admit/local axioms/unsafe, ~8,600 build jobs); "#print axioms" on both final theorems gives exactly [propext, Classical.choice, Quot.sound]. This bundle was also rebuilt from the exact public zip on separate hardware with the same result.

Argument. Immediately after a multiple of the least common multiple of $n+1,\ldots,2n-1$, each of the next $n-1$ integers past the first $n$ has a divisor in $(n,2n)$, so a window of length $n$ fails for every $\epsilon<1$; this also shows that no length that is $o(n)$ can work. Quantitatively, a sufficient window of length $y$ placed over those $n-1$ integers must satisfy $n-1\le\epsilon y$, so $y(\epsilon,n)\ge(n-1)/\epsilon$ and the constant in the linear order is at least about $1/\epsilon$. For the upper bound, the write-up counts, for $m$ in the window with a divisor $d\in(n,2n)$ and $m=dk$, the primes of $S_\epsilon$ dividing $d$, $k$ and $m$: writing $U(m)$ for the number of primes of $S_\epsilon$ dividing $m$ and $W(m)$ for $U(m)$ plus the number whose square divides $m$, the inequality $U(d)+U(k)\le W(dk)$ puts every such $m$ into one of three classes, a low count for $d$, a low count for $k$, or a high two-level count for $m$. Each class is periodic modulo $Q_\epsilon$, and second-moment (Chebyshev) and first-moment (Markov) estimates over a period bound it on every window of length at least $n(Q_\epsilon+2)$, with one period of boundary loss; the three bounds add up to at most $152y/\mu$ with $\mu=\sum_{p\in S_\epsilon}1/p$, which is below $\epsilon y$ by the choice of $S_\epsilon$. The write-up says that global density estimates, such as Ford's theorem on integers with a divisor in a given interval, do not control exceptional translates, which is why a local, periodic statistic is used instead.

Reading of the question. The site's remarks say that the quantifier on $x$ is not clear. The claim fixes the reading in which the bound holds for every $x$ and every length at least $y$, and treats $\epsilon$ as fixed while $n\to\infty$; the formal-conjectures statement file of the problem (450.lean, at its commit of 2026-09-18) adopts the same reading of $x$ and of the window lengths, defines the threshold accordingly, leaves its exact value open, and records the upper bound as a solved auxiliary statement with this claim's Lean file as its formal proof. The pull request of 2026-08-07 that added that record (formal-conjectures #4588) kept the headline question open on the ground that the problem asks for the best possible bound and the proof gives the order rather than the optimal constant, an outside judgment that the result is partial; the fix of 2026-09-12 (#5786) restated the headline as the threshold $y(\epsilon,n)$ itself. This page records the claim with scope partial: it determines the order of $y(\epsilon,n)$ in $n$ under one reading of the quantifier on $x$, which neither the source nor the site's curator fixes, and it leaves the exact threshold open. The dependence of the constant on $\epsilon$ is left open by the write-up itself: the lcm construction above puts it at least about $1/\epsilon$, and the explicit length gives at most $Q_\epsilon+2$. The regime in which $\epsilon$ shrinks with $n$ is outside the claim.

Covers. For fixed $0<\epsilon<1$ as $n\to\infty$, under the reading that the bound holds for every translate $x$ and every length at least $y$, the order $y(\epsilon,n)=\Theta_\epsilon(n)$. Not covered: the reading over typical $x$, the exact threshold and its dependence on $\epsilon$, and $\epsilon$ shrinking with $n$.

Formal verification by the author. The downloadable bundle linked above holds a Lean 4 project against a pinned Mathlib with the theorems turanLinearAnswer_isSufficientScale (the upper bound, for the explicit length $n\cdot(\prod_{p\in S}p^2+2)$) and sufficientScale_eventually_gt_n (every sufficient scale exceeds $n$ eventually for $0<\epsilon<1$). The solution page reports a build of about 8,600 jobs with a checker that rejects sorry, admit, local axioms and unsafe declarations, and an axiom report of propext, Classical.choice and Quot.sound for both theorems; the forum entry adds that the bundle was rebuilt from the public archive on separate hardware with the same result. A copy of the project's main file is the fourth link, at the commit of 2026-07-30 that the formal-conjectures file pins; that repository's index lists it under Colin Snyder's name as faithful to the statement file's target, with the repository's continuous-integration build and axiom audit as its verification, and the formal-conjectures pull request of 2026-08-07 reports that the linked theorem was read against the statement file's definitions and matches them. Neither check examines the mathematics, and none of this has been built or audited here, so no formalized evidence is listed.

Claimant and system. Colin Snyder, posting under the forum account coffeewithcolin, submitted the claim on 2026-07-15; the forum's tab names GPT 5.6 in a custom harness as the system used. The solution page carries no author line; its refereeing paragraph is the report of a second agent run that rebuilt the project and compared the formal definitions with the problem text, not a review by a named person.

Standing. Posted on the problem's forum on 2026-07-15. The claim carried eight comments, an exchange between a forum commenter and the claimant: whether the result conflicts with the site's remarks (the claimant answers that a sufficient $y$ exists for every fixed $\epsilon$ by periodicity and Ford's theorem, and that two conditions in the remarks read reversed), and whether the remarks' lcm construction already gives the linear order (the claimant answers that it gives the lower bound only, so that $y(\epsilon,n)$ cannot be smaller than about $n/\epsilon$, and that the upper bound is the new content). As of that date the site's curator had not commented and the problem's label was unchanged; no refereed publication is known here. The two outside checks recorded above, the formal-conjectures reading of 2026-08-07 and the lean-proofs index of 2026-07-30, examined the formal statement and the build, not the mathematics, and the first judged the headline question open, so no acceptance is recorded and the claim is claimed.