Problem 480

Let $x_1,x_2,\ldots\in [0,1]$ be an infinite sequence. Is it true that

\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq 5^{-1/2}\approx 0.447?

Source: erdosproblems.com/480

Number theory

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN), the site's label (page last edited 28 December 2025), credited to Chung and Graham [ChGr84]; the accepted claim page is Chung and Graham 1981. Theorem 1 of the chapter (Finite and Infinite Sets, Colloq. Math. Soc. János Bolyai 37, North-Holland 1984; p. 182; no file held) gives, for every sequence $\bar x$ in $[0,1]$ , $C(\bar x)\le(1+\sum_{k\ge1}F_{2k}^{-1})^{-1}=\alpha=0.39441967\ldots$ , and $\alpha<5^{-1/2}=0.44721\ldots$ , so the answer is yes with a smaller constant; their Theorem 2 shows $\alpha$ is best possible. The same theorems were announced without proof in [ChGr81] (Proc. Natl. Acad. Sci. USA 78 (1981), 4001; no file held), the authors' own first publication. The claim is accepted on the refereed announcement, which carries no proof, and on the curator's credit; the chapter is a proceedings chapter not shown to be refereed, and the 1980 monograph's added-in-proof note reports the theorem too. The "(Lean)" suffix is a catalog label explained under Formalization below; the Lean file is a formalization link on the claim page and gives no evidence here.

ChGr84: Chung, F. R. K. and Graham, R. L., On irregularities of distribution. In: Finite and Infinite Sets (Eger, 1981), Colloq. Math. Soc. János Bolyai 37, North-Holland (1984), 181--222, DOI 10.1016/B978-0-444-86893-0.50016-4. Theorem 1, p. 182; Theorems 2--3, p. 183; the proof of Theorem 1, p. 211; the extremal sequence, pp. 212--219; remarks, pp. 219--221. The site's thread links an image-only scan of the 42 pages on the second author's publication page. Library home: Chung and Graham 1984.
ChGr81: Chung, F. R. K. and Graham, R. L., On irregularities of distribution of real sequences. Proc. Natl. Acad. Sci. USA 78 (1981), no. 7, 4001, DOI 10.1073/pnas.78.7.4001 (communicated 13 April 1981; PubMed Central PMC319712). Theorems 1--3 stated without proof. A copy is on the first author's publication page. Library home: Chung and Graham 1981.
ErGr80: Erdős, P. and Graham, R. L., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique 28, Université de Genève (1980). Printed p. 96 and the added in proof, item (iii), printed p. 107. Library home: Erdős and Graham 1980.
dBEr49: de Bruijn, N. G. and Erdős, P., Sequences of points on a circle. Indag. Math. 11 (1949), 46--49. Library home: de Bruijn--Erdős 1949; the chapter's introduction reports its measure $\omega(\bar x)\le1/\log4$ . - Leads: the two later Chung--Graham papers the site's thread links from the second author's publication page (a sequence of points on a circle of circumference 1; sequences in $[0,1]^d$ ), and the citing records that Semantic Scholar lists for [ChGr81] (ten, among them arXiv:2511.14637 of 2025 and a 2018 paper in J. Number Theory on well dispersed sequences in $[0,1]^d$ ).

Problem 480

Status

Proof claims

Discussion