---

Claim. For every $n\geq 0$ and every $d\geq 1$ there is a $k\geq 1$ with

$$d \mid p_{n+1}+p_{n+2}+\cdots+p_{n+k},$$

where $p_r$ is the $r$th prime. This answers Problem 427 in the affirmative. Cédric Pilatte observed that the statement follows from a theorem of Shiu: for every $l\geq 1$ and every pair $a,q$ of coprime integers there are infinitely many runs $p_m,p_{m+1},\ldots,p_{m+l-1}$ of $l$ consecutive primes, all congruent to $a$ modulo $q$. The deduction takes $l=q=d$ and $a=1$. Choose such a run $p_m,\ldots,p_{m+d-1}$ with $m>n+1$, and let $r\in\{1,\ldots,d\}$ be the residue of $p_{n+1}+\cdots+p_{m-1}$ modulo $d$, with $r=d$ when that sum is already divisible by $d$. Each prime of the run adds $1$ to the sum modulo $d$, so appending the first $d-r$ primes of the run makes the sum divisible by $d$: the run $p_{n+1},\ldots,p_{m+d-r-1}$ works, with $k=m+d-r-1-n\geq 1$.

Acceptance. The site's curator, Thomas F. Bloom, marks Problem 427 proved and credits Pilatte's observation, with the deduction above displayed as the site's remark; that credit is the reviewed evidence. Shiu's theorem is refereed, D. K. L. Shiu, Strings of congruent primes, J. London Math. Soc. (2) 61 (2000), no. 2, 359–373, but the deduction itself is a site remark and no journal publication of it is recorded, so no refereed evidence is listed. The page is dated by the earliest archived capture that shows the label and the remark: the Wayback Machine capture of the site's primes tag page of 25 May 2024, which lists the problem as solved with Pilatte's remark. The site's full problem list captured on 1 March 2024 shows the problem without the remark, so the remark was first posted between those dates; the site's own revision history begins later and records no date for it. The capture of the problem's own page of 13 July 2024 is the second record. A correction to the index of the last prime in the displayed deduction was posted in the site's discussion in January 2026 and is incorporated above.

Formalization. Three Lean developments prove the statement, each naming Pilatte's deduction and Shiu's theorem as the informal source, so they are links on this page and not claims of their own. The first, posted in the site's discussion on 26 April 2026 by John Jennings and written with Aristotle (Harmonic), proves the statement from Shiu's theorem taken as an axiom. The second, Erdos427.lean in Boris Alexeev's lean-proofs repository, pinned at the commit of 25 August 2026 in the link, is unconditional: its header names Pilatte and Shiu as informal authors and Aristotle and John Jennings as formal authors, and it derives Shiu's theorem from the Maynard–Tao theorem in the form of Banks, Freiberg and Turnage-Butterbaugh, which the repository's Util.MaynardBFT development proves on the BoundedGaps library of FormalPantheon. The third, problems/427/Erdos427.lean in the Jayyhk/erdos-lean repository, pinned at the commit of 31 August 2026, is the file that the formal_proof attribute of the statement in google-deepmind/formal-conjectures names: a single-file vendoring of the same development, 127,701 lines, whose theorem erdos_427 (n d : ℕ) (hd : 1 ≤ d) gives, with primes indexed from zero, a $k\geq 1$ with $d$ dividing the sum of the $k$ primes from the $(n+1)$st on; the file contains no sorry token. This corpus has built none of the three, so no formalized evidence is listed. The formal-conjectures statement file is itself a statement with sorry and is not a formalization link.

Depends on. Nothing beyond the cited paper.