---

Claim. For every sequence $z_1,z_2,\ldots\in[0,1]$ there is an interval $I\subseteq[0,1]$ with

$$\limsup_{N\to\infty}\lvert D_N(I)\rvert=\infty, \qquad D_N(I)=\#\{n\le N: z_n\in I\}-N\lvert I\rvert,$$

so the answer to Problem 255 is yes. Schmidt's 1968 paper, the first of his series on irregularities of distribution, proves more: the set of $x$ for which $D_N([0,x))$ stays bounded in $N$ has Lebesgue measure zero, so almost every anchored interval answers the question. Two later refereed results sharpen this and have their own claim pages: part VI of the series (Schmidt 1972) shows that the set of such $x$ is at most countable, and Tijdeman and Wagner (Tijdeman and Wagner 1980) give the essentially best possible rate of growth at almost every anchor.

Depends on. Nothing in this wiki; the result rests on the cited paper alone.

Dating. The page is dated by the publication year. The journal record (Quart. J. Math. Oxford Ser. (2) 19 (1968), 181–191) gives no day, and the day in the page name is a placeholder.

Acceptance. Refereed: Quart. J. Math. Oxford Ser. (2) 19 (1968), 181–191. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED (LEAN) and records the answer as yes, proved by Schmidt, in the problem's commentary; the site's thread held no comment and no proof claim as of 2026-10-07, and the community database lists the problem as proved. The measure-zero statement above is the one part VI (Schmidt 1972) recalls as the result it sharpens.

The Lean qualifier. The site labels the problem PROVED (LEAN) and the community database records the status as "proved (Lean)", but neither names a formal proof, and the problem page records no formalized statement in formal-conjectures. The file src/latest/ErdosProblems/Erdos255.lean of Boris Alexeev's lean-proofs repository (GitHub plby/lean-proofs), linked above at a pinned commit and first added on 17 August 2026, declares itself a Lean formalization of a solution to the problem, with Schmidt as its informal author and Codex and GPT-5.6 Sol as its formal authors; it proves erdos_255, that for every sequence in $[0,1]$ some anchored interval $[0,x)$ has infinite $\limsup$ of the absolute discrepancy, and it is most likely the proof the site's qualifier refers to. It is not built or audited here and has no fidelity review, and its AI-tool authorship is provenance only, so the evidence of this claim is the refereed paper and the curator's acceptance, not a formalization.