---

Claim. With $t_k(n)$ the least positive $m$ such that $n$ divides $m(m+1)\cdots(m+k-1)$, both questions of Problem 394 have the answer yes: $\sum_{n\le x}t_2(n)\ll x^2/(\log x)^c$ with the explicit constant $c=1/2048$, and $\sum_{n\le x}t_{k+1}(n)=o(\sum_{n\le x}t_k(n))$ for every fixed $k\ge2$. The write-up is A proof of Erdős Problem 394, hosted on the Star Fleet Math site and submitted by Colin Snyder to the site's proof-claims tab on 2026-07-15 as a full proof claim; the page itself carries no date or byline. By the claim's summary and the write-up, a prime $p\ge k$ has $t_k(p)=p+1-k$, so any saving exists only on average; an explicit finite Brun sieve over medium primes bounds the sum of $t_{k+1}$, attaching one large prime to each selected modulus gives a lower bound for the sum of $t_k$ with an extra Euler factor $\prod_p(1+1/(Kp))$, an exact inequality between powers of the two Euler products converts that extra factor into the logarithmic separation, and a grid of cutoffs $X_N=16^N$ extends the estimate from the grid to every real cutoff. This page rests on the write-up's statements and its description of the method; the proof was not checked here.

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:

For $t_k(n)$ the least positive $m$ with $n\mid m(m+1)\cdots(m+k-1)$, we claim both answers are yes:

$$\sum_{n\le x}t_2(n)\ll\frac{x^2}{(\log x)^c}\ > \text{with explicit }c=\tfrac{1}{2048},\\ \sum_{n\le > x}t_{k+1}(n)=o!\left(\sum_{n\le x}t_k(n)\right)\ \text{for every fixed > }k\ge2.$$

Proved in Lean 4 / Mathlib, standard axioms only, no sorry. Idea:

primes force $t_k(p)=p+1-k$, so the saving only exists on average. An explicit finite Brun sieve over medium primes bounds the $t_{k+1}$ sum, while attaching one large prime to each selected modulus gives a lower bound for the $t_k$ sum with an extra Euler factor $\prod_p(1+\tfrac1{Kp})$. The two Euler products obey an exact powered gap, $(A/E)^M\le B^{M+1}$, and carrying that identity intact converts the extra power into the logarithmic separation. A dense grid $X_N=16^N$ then upgrades the estimate to every real cutoff, not just a subsequence. Notes: Verify: unzip (106 Lean files), run the included verifier; "#print axioms" on the two final theorems gives exactly [propext, Classical.choice, Quot.sound]. The constant $c=1/2048$ is explicit in the formal statement, and the little-o conclusion is stated with Mathlib's IsLittleO over all real cutoffs.

Formalization. The claim's notes say the result is proved in Lean 4 with Mathlib across $106$ files with no sorry and standard axioms only, the two final theorems reporting exactly propext, Classical.choice and Quot.sound under #print axioms, the constant $1/2048$ explicit in the formal statement and the little-o conclusion stated with Mathlib's IsLittleO over all real cutoffs; the hosted write-up says an independent rebuild against a clean pinned Mathlib passed. The development is distributed as the archive linked above and is also hosted, as a copy of the Star Fleet proof added on 2026-07-23, in the starfleet/erdos-394 folder of the williamjblair/lean-proofs repository at the pinned commit, whose Research/FirstQuestion.lean ends with the theorem erdos394_first_question_proved (the bound $7680x^2\exp(-\log\log x/2048)$ for large $x$, so $c=1/2048$) and whose Research/DenseHierarchyLittleO.lean holds the second question; that repository's README describes a build gate with an axiom audit on every push. The formal-conjectures file for the problem marks both parts research solved and points its formal_proof attributes at those two files (edits of 2026-08-07, 2026-08-24 and 2026-09-11), which records the formal statement's status and is not a formalization link of its own. Nothing was built or audited here, and the formal statements were not compared with the problem's, so the page lists no formalized evidence.

Standing. The claim is pending. The site's label is open, last edited 2025-10-28, before the claim, and the curator has not credited the result, so there is no acceptance evidence. The claim's tools field names the AI system GPT 5.6 in a custom harness. No comment had been posted on the claim. Pickhardt's later partial proof claim, recorded on the problem page, claims the lower bound $\sum_{n\le x}t_2(n)\gg x^2/((\log x)^{1/2}\log\log x)$, which would leave no exponent $c>1/2$ possible in the first question; it is consistent with $c=1/2048$ and refers to this claim as settling the first question.