---

Claim. For every sequence $\bar x=(x_1,x_2,\ldots)$ in $[0,1]$,

$$C(\bar x)=\inf_n\liminf_{m\to\infty}n\lvert x_{m+n}-x_m\rvert \le\Bigl(1+\sum_{k\ge1}\frac1{F_{2k}}\Bigr)^{-1}=\alpha=0.39441967\ldots,$$

where $F_n$ are the Fibonacci numbers, $F_0=0$, $F_1=1$, $F_{n+2}=F_{n+1}+F_n$. This is Theorem 1 of the 1984 chapter (p. 182), quoted on the result page theorem_1; its Theorem 2 (p. 183, theorem_2) exhibits a sequence $\bar x^*$, built from the digits of $n$ in the even-indexed Fibonacci numbers, with $C(\bar x^*)=\alpha$, so the constant is best possible. Since $\alpha<5^{-1/2}=0.44721\ldots$, the question of Problem 480 has the answer yes, with a smaller constant than the one asked. The digest is on the source card chung_1984_irregularities_distribution. The same three theorems were announced without proof in the 1981 note (its Theorem 1; card chung_1981_irregularities_distribution_real_sequences), the authors' own first publication, which dates this page; the 1980 monograph of Erdős and Graham, the second author's own, had reported the theorem as just proved. The chapter proves Theorem 1 as a corollary of Theorem 3, the exact value of a permutation extremal problem (p. 211), and Theorem 2 through the extremal sequence (pp. 212--219); the 42-page proof is recorded for structure only and is not checked here.

Formalization. The site's "(Lean)" suffix refers to the file Erdos480.lean in Boris Alexeev's repository, linked above at its commit of 7 September 2026; its header names Fan Chung and Ronald Graham as the informal authors and the AI systems Codex and GPT-5.6 Sol as the formal authors, so it is a formalization link on this page and not a claim of its own. Its theorem proves the site's inequality from a finite statement, that among any thirteen consecutive terms some pair $n\le12$ apart has $n\lvert x_{m+n}-x_m\rvert\le3/7$, together with $3/7<5^{-1/2}$; it does not prove the constant $\alpha$. Third-party Lean, not built or audited here, so no formalized evidence is listed. The formal-conjectures statement file the problem page records is a statement, not a formalization.

Acceptance. Refereed: F. R. K. Chung and R. L. Graham, On irregularities of distribution of real sequences, Proc. Natl. Acad. Sci. USA 78 (1981), no. 7, 4001 (July 1981; communicated 13 April 1981), which states the theorems and carries no proof. The proof, On irregularities of distribution, in Finite and Infinite Sets (Eger, 1981), Colloq. Math. Soc. János Bolyai 37, North-Holland (1984), 181--222, is a proceedings chapter not shown to be refereed, so the proof's acceptance rests on the curator's credit. Reviewed: the site's curator, Thomas F. Bloom, marks Problem 480 PROVED (LEAN) and credits the chapter with the proof in the problem's commentary (page last edited 28 December 2025); the curator neither wrote nor submitted the result. The 1980 monograph of Erdős and Graham reports the theorem as just proved in its added-in-proof note (p. 107). The page is dated by the first day of the issue month of the announcement, since the record gives no finer posting date.