---

Claim. The site's wording of Problem 998 is false: for $\alpha=\sqrt2/10$, $u=1/4$ and $v=u+\alpha$, the count $\#\{1\le m\le n:\{\alpha m\}\in[u,v)\}$ differs from $n(v-u)$ by at most $1$ for every $n$, while $u$ is rational and so not of the form $\{\alpha k\}$ for any integer $k$. The proof is the Lean development in Boris Alexeev's repository of formalized Erdős problems, added on 2026-08-17 and linked above at the commit of 2026-08-24 that last touched the file. Its theorem not_erdos_998 is the negation of the universal statement: it is not the case that for every irrational $\alpha$ and every $0\le u<v\le1$ satisfying the eventual $O(1)$ condition (HasBoundedRemainder), both $u$ and $v$ are fractional parts of integer multiples of $\alpha$. The bound comes from a telescoping fractional-part identity for a translate of an interval of length $\{\alpha\}$, the mechanism of Ostrowski's 1927 estimate; the file imports only Mathlib, contains no sorry and prints the theorem's axioms. Its module comment says that the endpoint formulation copied into the problem is false and that Kesten's theorem characterizes bounded-remainder intervals by their length.

Claimant and standing. The file's header names Harry Kesten as informal author and Codex and GPT-5.6 Sol as formal authors. Kesten's paper proves the length criterion and states no such counterexample, so the development is recorded as its own result, under the repository owner's slug, rather than as a formalization of a published claim; the Kesten page records Kesten's Theorem 4, which proves the corrected Statement. The page is rejected because it answers the site's wording, the endpoint converse Erdős printed in 1964, not the corrected Statement, which asks only that the length $v-u$ be a fractional multiple of $\alpha$; the result itself is not in question and is credited in the problem page's Notes. The site (accessed 2026-09-04) labels the problem PROVED and does not mention the development, the community database at teorth/erdosproblems lists the problem as not formalized, no outside reviewer has examined the file, and this corpus has not built or audited it, so it carries no formalized evidence.

Depends on. No page of this wiki.