---

Claim. The theorem erdos_492 of the Lean development Erdos492.lean, added to Boris Alexeev's repository of Lean proofs on 2026-08-20 and linked above at a pinned commit, states that for every positive, strictly increasing sequence of natural numbers whose consecutive ratios tend to one, for almost every real $\alpha>0$ the positions of $\alpha,2\alpha,3\alpha,\ldots$ within the gaps of the sequence are uniformly distributed in $[0,1)$. That is the site's wording of Problem 492, with $A\subseteq\mathbb N$. The module docstring says that under this hypothesis the answer is positive because the counting hypothesis of Davenport and Erdős is automatic, and that Schmidt's negative example concerns the formulation with real subdivision points; the theorem's docstring calls it the resolution of Problem 492 for the statement printed with natural-number subdivision points. The file's header presents it as a Lean formalization of a solution to the problem, names Wolfgang M. Schmidt as its informal author and the AI systems Codex and GPT-5.6 Sol as its formal authors; the submitter of the repository is the claimant here.

Depends on. No page of this wiki.

Covers. The corrected Statement of Problem 492 for every infinite set of positive integers $A$ with $a_{i+1}/a_i\to1$, which is the site's wording. The integer case is a special case of the corrected Statement and the site's wording in full, so the claim is partial rather than rejected. The case lies inside the sparse case on [[problems/number_theory/E0492/claims/1963_01_01_davenport_erdos|the Davenport--Erdős page]], and the corrected Statement as a whole is disproved on Schmidt's page. The problem page's Notes credit the result.

Standing. The Lean file is third-party work that this corpus has not built or audited, so it gives a formalization link and no formalized evidence.