---

Claim. With $S_N(\alpha)=\sum_{k\le N}(\tfrac12-\{k\alpha\})$ and $\alpha$ uniform on $(0,1)$, $S_N(\alpha)/\log N$ converges in distribution to the centered Cauchy law of scale $1/(2\pi)$, so the distribution functions converge at every real $c$ to $\tfrac12+\pi^{-1}\arctan(2\pi c)$. This answers Problem 1002 yes, with the same limit as Kwon's independent manuscript on Kwon's claim page. The result is Theorem 1.1 of Shouqiao Wang, A proposed solution to Erdős Problem 1002, first posted to the author's GitHub repository on 2026-07-21 and submitted to the problem's proof-claims thread the same day (the discussion link); the preprint link pins the paper (44 pages) at the repository commit of 2026-07-24, the last that touched the problem's folder as of 2026-10-07. The card wang_2026_proposed_solution_erdos_problem_1002 holds the digest. The paper states that the solution was found by an AI system (GPT-5.6 Sol, as the claim's thread entry names it; the paper says GPT-5.6), and the thread entry that it was checked by AI reviewers.

Submission note. Posted to erdosproblems.com as a proof claim by Shouqiao Wang (account ShouqiaoWang) on 21 July 2026, giving "GPT-5.6 Sol" as the AI used:

The answer is yes. If $\alpha$ is uniform on $(0,1)$, then

$$> \frac{1}{\log N}\sum_{k\le N}\left(\frac12-{k\alpha}\right) >$$

converges to a centered Cauchy law with scale $1/(2\pi)$. Tao suggested that the large fluctuations should come from occasional large digits in the continued fraction of $\alpha$. That is what the proof finds. Up to an error much smaller than $\log N$, the sum is rewritten in terms of rational approximations $q/p$ to $\alpha$. The ordinary approximations cancel when added together. What remains are the cases where $p\alpha$ is extremely close to an integer, corresponding to continued-fraction denominators with a large next digit. There are only a few such events, and they approach a Poisson process. The quantity $N(p\alpha-q)\bmod 1$ also becomes uniform. Each event contributes roughly $1/\xi$, where $\xi$ measures the closeness, and adding these rare contributions gives the Cauchy law. Notes: The solution is found by GPT-5.6 Sol. Checked by AI reviewers. I'll submit the Lean formalisation soon!

Argument, as the paper describes it. The sum is reconstructed in $L^2$, up to $o(\log N)$, as a sum of "shots" indexed by primitive rational approximations to $\alpha$; a Ramanujan-sum square-function estimate removes the nonresonant shots; the remaining signed, marked resonances, the continued-fraction denominators followed by a large partial quotient, converge to a marked Poisson process by a rare-event theorem proved in the paper, with the mark $N(p\alpha-q)\bmod1$ made uniform by a cylinder oscillation argument rather than by averaging the starting point; the Poisson integral has Cauchy scale $1/(2\pi)$.

The formal statement. The formalization link is the folder 1002/lean of the same repository at the same commit: a Lean 4 project under Lean v4.27.0 with Mathlib pinned at its v4.27.0 tag, about 250 source files. Erdos1002/Statement.lean defines the sawtooth $\tfrac12-\{x\}$, the sum over Finset.Icc 1 N, the normalization by Real.log N, the Lebesgue measure of $\{\alpha\in(0,1):\ldots\le c\}$ and the Cauchy distribution function $\tfrac12+\pi^{-1}\arctan(2\pi c)$; VerifiedMain.lean proves erdos1002, pointwise convergence of the distribution functions to that limit for every real $c$, and OfficialStatementBridge.lean derives erdos1002_official, the existential form with a monotone $g$ tending to $0$ and $1$, matching the problem's wording and the formal-conjectures statement; Audit.lean prints the axioms of both. The author added the formalization to the thread entry on 2026-07-24. A second posting of the same formalization is src/latest/ErdosProblems/Erdos1002.lean in Boris Alexeev's repository https://github.com/plby/lean-proofs (the second formalization link, pinned at the commit of 2026-09-15; the file was added on 2026-08-26): it imports a port of Wang's development to a later Lean toolchain, whose Statement.lean matches Wang's apart from added options, and re-exports erdos1002_official and erdos1002 as erdos_1002 and erdos_1002_cauchy; the file carries no attribution header.

Outside examination. The record link is a report by Millennium Research (Ibrahim Mian and Shayaan Siddique), published 2026-08-01 and amended 2026-08-02, which rebuilt the Lean development at the repository commit of 2026-07-28 (whose 1002/ folder is the one pinned here) on their own hardware, swept every theorem of the compiled namespace for axioms (exactly propext, Classical.choice and Quot.sound), scanned the sources for escapes, compiled a bridge theorem deriving the formal-conjectures rendering of the problem from erdos1002_official, replayed the modules through lean4checker, and rebuilt once more under a toolchain compiled from source; it reads the formal statement as faithful to the site's question and treats the prose paper only as commentary. The report's authors then joined Kwon's formalization project, which it discloses. The site labels the problem OPEN and the thread carries no curator comment; comments from both claimants (2026-07-24) affirm that the two proofs were developed independently, with Kwon's answer public first.

Acceptance. Formalized. This corpus's verification built Boris Alexeev's repository at the commit of 2026-09-15 that the second formalization link pins (its src/latest project, Lean v4.33.0 with Mathlib v4.33.0; the module ErdosProblems.Erdos1002 and the comparator challenge ComparatorChallenges/ErdosProblems/Erdos1002.lean) and checked the axioms of Erdos1002.erdos_1002 and Erdos1002.erdos_1002_cauchy, which are exactly propext, Classical.choice and Quot.sound. What was built is that repository's port of Wang's development, revised there after it was first added: between the commits of 2026-08-26 and 2026-09-15, 138 files of its ErdosProblems/Erdos1002/ folder changed, while Statement.lean, OfficialStatementBridge.lean, VerifiedMain.lean, the re-exporting file and the challenge did not. Wang's own folder, the first formalization link, was not built here, so the build certifies the port's proof of the two statements, not Wang's files. The challenge pins both declarations, whose statements import only Mathlib, and the fingerprint of each was found identical to the challenge; the challenge enables no second kernel checker, so the acceptance rests on Lean's kernel, the axiom check and the fingerprint. The statements were audited clause by clause against the problem's Statement and the claim above. erdos_1002 asserts a monotone $g$ with limits $0$ at $-\infty$ and $1$ at $+\infty$ such that, for every real $c$, the Lebesgue measure of the set of $\alpha\in(0,1)$ with $(\log n)^{-1}\sum_{k=1}^{n}(\tfrac12-\{\alpha k\})\le c$ tends to $g(c)$, with the fractional part as Int.fract and the natural logarithm: the site's question, answered yes. erdos_1002_cauchy pins the limit as $\tfrac12+\pi^{-1}\arctan(2\pi c)$, the centered Cauchy law of scale $1/(2\pi)$, exactly this page's claim, so neither statement can hold for a degenerate reason, and the junk values of the normalization at $n\le1$ cannot affect a limit. Not reviewed: the site labels the problem OPEN, its curator has not commented on the claim, and the outside report above is a mechanical check by two named persons rather than a referee's report or the curator's acceptance. Not refereed: there is no journal or arXiv version.

Depends on. Nothing in this wiki.