---

Alexeev, Putterman, Sawhney, Sellke and Valiant proved (Theorem 4.1 of the paper on the 2026 card) that for every real $\alpha$ the sequence $\{\alpha p_n\}$ over the primes is not well-distributed in the sense of Hlawka and Petersen. This answers the question of Problem 997 yes. The paper attributes the proof to an internal OpenAI model, with the human authors editing the write-up. The argument approximates $\alpha$ by a rational $a/q$ through Dirichlet's theorem and then takes, from the theorem of Banks, Freiberg and Turnage-Butterbaugh [BFT15] built on the Maynard–Tao sieve, a run of $m$ consecutive primes all in one residue class modulo $q$ and spanning a gap at most a constant times $q$; the fractional parts $\{\alpha p\}$ along the run cluster in a short interval, which a well-distributed sequence cannot allow for large $m$. The earlier existence result of Champagne, Lê, Liu and Wooley, one irrational (indeed transcendental) $\alpha$ rather than every $\alpha$, is the partial claim Champagne, Lê, Liu and Wooley 2024.

Depends on. Nothing in this wiki; the result rests on the cited preprint and the published theorem of Banks, Freiberg and Turnage-Butterbaugh.

Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem proved on the strength of this paper, with the page last edited 2026-04-01, and the discussion thread of 2026-04-01 carries a comment by Terence Tao stating that the problem is now solved and describing the argument, noting that a 2013 paper of Benatar (arXiv:1305.0348), by the same sieve machinery, essentially gives the case of Diophantine $\alpha$, one standard additional sieve estimate away, and that the present proof avoids a Diophantine condition by approximating $\alpha$ by a rational and using a congruence class. The formal-conjectures statement file ErdosProblems/997.lean (a sorry body at the pinned revision, the catalog's statement rather than a posting of the result) marks the problem research solved and points at the Lean proof below. The preprint (arXiv v1 2026-03-31, v2 2026-04-02) had no journal version found on 2026-10-07, so refereed is not listed.

Formalization. Pietro Monticone posted to the thread on 2026-04-01 a Lean 4 file (pinned above by its gist revision), writing that the solution was autoformalized by Aristotle, conditionally on the Banks–Freiberg–Turnage-Butterbaugh theorem taken as an axiom. The file proves erdos997 (α : ℝ) : ¬IsWellDistributed (fracSeq α) with that theorem declared as the axiom maynardTaoBFT; every other step is proved. The site's label PROVED (LEAN) rests on this file. The axiom is a published theorem (Acta Arith. 2015), but the formalization is conditional on it, its definition of well-distribution counts closed subintervals $[a,b]\subseteq[0,1]$ where the site's statement says intervals, and this corpus has not audited the Lean statement against the problem. A later version of the file, src/latest/ErdosProblems/Erdos997.lean in Boris Alexeev's repository (the revision of 2026-09-15, pinned in the link), states in its header that its formalization status is unconditional, names as informal authors an internal model at OpenAI and the five authors and as formal authors Aristotle and Pietro Monticone, imports a repository module whose MaynardBFT.consecutive_primes proves the Banks–Freiberg–Turnage-Butterbaugh statement in place of the axiom, and records in a closing comment that erdos_997 depends on the axioms propext, Classical.choice and Quot.sound. This public development claims an unconditional proof; it is not built or audited here, so formalized is not listed as evidence for either file.