---

Claim. The catalog erdosproblems.com labels Problem 998 PROVED (page last edited 2025-10-05, accessed 2026-09-04), and its curator, Thomas Bloom, credits the proof to Kesten. The paper credited is Harry Kesten, On a conjecture of Erdős and Szüsz related to uniform distribution mod 1, Acta Arith. 12 (1966), 193--212, whose card is kesten_1966_bounded_remainder; the year is the volume's journal header, where the site's record gives 1966/67. Its Theorem 4, transcribed on the theorem page, states: for fixed $\xi\in[0,1]$ and $0\le a<b\le1$ with $b-a<1$, the discrepancy $\#\{1\le m\le M:\{m\xi\}\in[a,b)\}-M(b-a)$ is bounded in $M$ if and only if $b-a=\{j\xi\}$ for some integer $j$. With $\xi=\alpha$ irrational, the necessity direction is the corrected Statement of Problem 998, which asks that bounded discrepancy force the length $v-u$, not the endpoints, to be a fractional multiple of $\alpha$; the sufficiency direction is the earlier theorem of Hecke and Ostrowski.

Acceptance. Refereed: the theorem is published in Acta Arith. 12 (1966). Reviewed: the erdosproblems.com page for Problem 998 is labeled PROVED by the site's curator, whose commentary says "This is true, and was proved by Kesten [Ke66]", crediting this paper. Kesten writes that the theorem "confirms a recent conjecture of Erdős and Szüsz [2]" and, in Section 4, that "except for a slight modification this was conjectured by Erdős and Szüsz ([2], p. 61)"; the modification is the passage from the two endpoints to the length, and the site's label and attribution adopt it, as the corrected Statement does. The site's wording is the endpoint converse that Erdős printed in 1964 as a conjecture of Erdős and Szüsz (the conjecture card). Alexeev's Lean development, which disproves the site's wording, is a rejected claim page, since it answers that wording rather than the corrected Statement.

Reconstruction. The paper's necessity proof is reconstructed on the theorem page only for the anchored case $[0,b)$ with irrational $\xi$; the arbitrary-translate reduction and the rational case are not reconstructed. The site's forum thread has no comments or proof claims (accessed 2026-09-04).

Formalization. Collin Yuanjie Ren's AI-assisted Lean development formalizes the length criterion: its root theorem Kesten.bounded_remainder_iff states, for irrational $\alpha$ and $0\le u<v\le1$, that the discrepancy of $[u,v)$ is eventually uniformly bounded exactly when $v-u=k\alpha+l$ for integers $k$ and $l$. Its README (the formalization link above, pinned to the commit the community database cites) says that the statement does not assert the separate-endpoint wording, that the historical theorem is due to Hecke, Ostrowski and Kesten, and that Alexeev's file proves a counterexample to the endpoint formulation; the community database at teorth/erdosproblems records the development in a note while listing the problem as not formalized. The development formalizes the theorem the site credits to Kesten, so it is a link on this page. This corpus has not built or audited it, so it gives no formalized evidence.

Depends on. Nothing in this wiki; the refereed theorem and its transcription are on the library pages linked above.