---

The question is answered yes. With $q(n,k)$ the least prime not dividing $\prod_{1\le i\le k}(n+i)$, the claim is that for some fixed $\epsilon>0$ infinitely many $n$ have $q(n,\log n)>(2+\epsilon)\log n$. The construction posted by the forum account Kevin Barreto on 2 March 2026 gives this for every fixed $0<\epsilon<3/\log4-2\approx0.164$, so the constant $2$ can be raised to any constant below $3/\log4\approx2.164$ (the endpoint itself is not attained), and a second argument posted the same day, using the prime number theorem, gives it for every constant in place of $2$. The first write-up is the anonymous four-page note recorded as Primes in a logarithmic block product: its Theorem 2.1 takes $\epsilon=1/10$, by the central binomial coefficient $\binom{2m}{m}$, which every prime in $(m,2m]$ divides, and a simultaneous approximation step that makes each prime of $(2m,3m]$ divide some term of the block; its Remark 2.4 extends this to every fixed $\epsilon<3/\log4-2$. The second write-up was not read. The idea, as Tao's elaboration in the thread (2 March 2026) puts it: the primes up to $k=\log n$ divide the block automatically; Erdős forced $n\equiv0$ modulo every prime in $(k,Ak]$ by the Chinese remainder theorem, which keeps $n\le e^k$ only for $A\le2-o(1)$; it suffices that $n$ lie within $k/2$ of a multiple of each such prime, which Dirichlet's approximation theorem achieves with $n$ small enough to allow $A$ as large as $\asymp\log k/\log\log k$. Carried through, with a factor $1/2$ lost in returning from a symmetric block to $\prod_{i=1}^k(n+i)$, this gives infinitely many $n$ with $q(n,\log n)>\frac{1-o(1)}{2}\frac{\log\log n}{\log\log\log n}\log n$ (Tao, 3 March 2026, confirming that a write-up posted that day by another contributor worked out this constant); that sharper bound is that write-up's claim, recorded on its own page, and not part of the accepted claim.

Submission note. Posted to the site's forum by Kevin Barreto on 2 March 2026:

GPT-5.2 Pro gives an extremely elementary argument for any $0<\epsilon<\frac{3}{\log 4}-2$ viewable as a PDF here. This is certainly a very easy problem as stated, so I am suspicious ([ErGr80] seems to state it this way as well). Going into [Er79d] seems to ask about the opposite direction inequality for sufficiently large $n$: "Is it true that $q(n,[\log n])<(2+\varepsilon)\log n$ for $n>n_0(\varepsilon)$?"

I suspect this is the actual intended direction? Anyhow, Aristotle did autoformalise its solution to the problem as stated on the site here. ChatGPT Deep Research failed to find anything substantive in the literature (sharing its chat link results in an error, but one can view its generated PDF report here). GPT-5.2 Pro failed at constructing an argument for the more general problem in the description.

Update: In an independent, again autonomous run, GPT-5.2 Pro has given an alternative argument utilising PNT that resolves the stated question for arbitrarily large $\epsilon$: See here.

(The site has been updated to address this comment.)

Provenance. The poster attributes the construction and its extension to GPT-5.2 Pro in two autonomous runs, and the formalization to Aristotle, Harmonic's automated prover; the site's commentary names the same model. No paper, preprint-server version or refereed publication exists: the written forms are the two documents on a file-sharing service linked above, whose identities are unstable (the first is pinned only by the bytes on its card), and the Lean files.

Acceptance. Reviewed: the site's curator, Thomas Bloom, who is independent of the claimant, marked the problem solved on 7 March 2026 (the thread's comment of 11:20 that day, and the label PROVED (LEAN)), after Tao, a named mathematician, endorsed the argument in the thread on 2 March 2026, calling it a case where Erdős posed a problem that was too easy, and elaborated it; Nat Sothanaphan reported a GPT standard check, as Sothanaphan calls it, that found no issues. This is documented acceptance by the site, distinct from refereeing: no refereed publication, arXiv version or written independent expert review was found on 2026-09-18 (the problem page's search scope). The site's suffix (Lean) is a catalog label: the file ErdosProblem457.lean at the commit linked above proves erdos_457 with $\epsilon=0.1$ from a main theorem with the constant $2.1$, and the collection formal-conjectures names it in a formal_proof attribute on its statement, whose body is sorry at the pinned commit; the file contains no sorry, axiom or native_decide. The second Lean link above is the file Erdos457.lean in Boris Alexeev's repository lean-proofs, whose header names GPT-5.2 Pro and Barreto as informal authors and Aristotle and van Doorn as formal authors, so it is a formalization of this claim and not an independent proof; it proves the same two theorems and records the standard axioms in closing comments. Neither file was built, kernel-checked or statement-audited here, so formalized is not listed. Read depth here: the thread's sketch read and not checked; the first write-up read in full, with claims checked for Theorem 2.1 and Remark 2.4; the second write-up not read; nothing independently reviewed by this project.

Scope. Full: the claim answers the Statement, the monograph's form. Erdős's 1979 paper asks the opposite inequality for all large $n$, a variant that the problem page's Formulation opens with, and this answer refutes his expectation there; the upper-bound question for $q(n,\log n)$ is Problem 1181, split off on 7 March 2026.