---

Claim. Let $S_n(\alpha)=\sum_{k=1}^{n}(\tfrac12-\{k\alpha\})$. For $\alpha$ uniformly distributed on $(0,1)$,

$$\frac{S_n(\alpha)}{\log n}\Longrightarrow \mathrm{Cauchy}\Bigl(0,\frac{1}{2\pi}\Bigr),$$

so that

$$\lim_{n\to\infty} \bigl\lvert\{\alpha\in(0,1):S_n(\alpha)/\log n\le c\}\bigr\rvert =\frac12+\frac1\pi\arctan(2\pi c)$$

for every real $c$. This answers Problem 1002 yes, with $g(c)=\tfrac12+\pi^{-1}\arctan(2\pi c)$ as the asymptotic distribution function; the site writes the summand with the same sign, and the manuscript notes that the sign convention is immaterial because $\alpha\mapsto1-\alpha$ preserves Lebesgue measure and negates the sum. The result is Theorem 1.1 of Sangyoon Kwon, A Cauchy limit for a sawtooth sum, first published on 2026-07-13 as a GitHub repository holding the manuscript and its source (the first preprint link, 16 pages at the commit of that day), and submitted to the problem's proof-claims thread on 2026-07-23 (the discussion link) after a moderator invited the posting; the thread records that the site's moderation policy on AI-assisted proofs had changed on 2026-07-14. The manuscript states that the answer was first obtained from an AI system (OpenAI GPT-5.6-sol Pro), that the proof was developed through iterative prompting of that model, and that another system (OpenAI Codex, GPT-5.6-sol) assisted with editing, compilation and consistency checks. A revised manuscript (version 11, dated 2026-08-25, 20 pages, the second preprint link, pinned to the revision branch's commit of 2026-09-02) keeps Theorem 1.1 unchanged.

Submission note. Posted to erdosproblems.com as a proof claim by Sangyoon Kwon (account ronut01) on 23 July 2026, giving "OpenAI GPT-5.6-sol Pro; OpenAI Codex (GPT-5.6-sol)" as the AI used:

I propose a complete solution to Problem #1002. Let

$$> S_n(\alpha)=\sum_{k=1}^{n}\left(\frac12-\{k\alpha\}\right).$$

For

Lebesgue-uniform $\alpha\in(0,1)$, the manuscript proves

$$> \frac{S_n(\alpha)}{\log n} \Longrightarrow > \operatorname{Cauchy}\!\left(0,\frac1{2\pi}\right), \qquad > g(c)=\frac12+\frac1\pi\arctan(2\pi c).$$

An exact Euclidean-algorithm

reciprocity formula rewrites $S_n$ as an alternating continued-fraction cost. Continued-fraction coordinates split each summand into a heavy-tailed Gauss digit marked by a rapidly oscillating torus coordinate and a bounded carry remainder. Complete-cylinder oscillation and a resonance decomposition yield the Poisson limit for the large jumps, while small-jump estimates and a Gauss-torus carry/reset construction control the remainder. Stopping-time estimates and the exact symmetry $S_n(1-\alpha)=-S_n(\alpha)$ complete the proof and remove deterministic centering. Notes: Following the moderator’s invitation, I am submitting this independent proof claim and noting that the write-up and its public GitHub repository have been online since 13 July 2026. Repository: https://github.com/ronut01/erdos-problem-1002-cauchy-limit Initial public commit: https://github.com/ronut01/erdos-problem-1002-cauchy-limit/commit/5f00aa94bc6a725e8e93332e0d71b17752936100 AI-use disclosure: The proposed solution was generated and developed using OpenAI GPT-5.6-sol Pro. OpenAI Codex (GPT-5.6-sol) assisted with editing, compilation, and automated consistency checks.

Argument, as the manuscript describes it. An exact reciprocity formula along the Euclidean algorithm, $S_N(x)=-S_m(Tx)+\Phi(x,u)$ with $T$ the Gauss map, $m=\lfloor Nx\rfloor$ and $u=\{Nx\}$, writes $S_n$ as an alternating sum of continued-fraction costs; each summand splits into a heavy-tailed Gauss digit marked by a rapidly oscillating torus coordinate and a bounded carry. A Poisson limit for the large marked digits is proved by integrating Fourier modes over complete continued-fraction cylinders, since the initial measure sits on the graph $\alpha\mapsto(\alpha,\{n\alpha\})$ and plain Gauss-map mixing does not apply; the carry is handled through a Gauss-torus cocycle with a reset argument, and the symmetry $S_n(1-\alpha)=-S_n(\alpha)$ removes any centering.

Formalization. A separate repository, the formalization link (pinned to its commit of 2026-09-03, Apache-2.0), states in Kwon1002/Statement.lean both the concrete Cauchy limit and the existential distribution-function form the problem asks for, and its README reports that the main theorem depends on exactly propext, Classical.choice and Quot.sound under Lean v4.27.0 with Mathlib v4.27.0, with a rebuild from source on another machine. The README names it a collaborative companion project of Kwon with Ibrahim Mian and Shayaan Siddique (Millennium Research), says that one large-deviation estimate is proved there by a different route from the manuscript's, by agreement with the author, and that shared Gauss-transfer infrastructure is reused from Wang's development; Kwon announced it on the thread on 2026-09-02. No build, replay or audit of it is recorded in this repository.

Outside examination. The record link is a report by Millennium Research (Mian and Siddique), published 2026-08-01 and amended 2026-08-02, before the collaboration above began, which the report discloses. For this manuscript it records a reading audit of every numbered result, finding no fatal error and one expositional imprecision (Proposition 6.4), and labels that verdict as not machine-checked; its mechanical layers concern Wang's Lean development, recorded on Wang's claim page. The report also states that the two proofs are architecturally independent, which both claimants affirmed on the thread (2026-07-24).

Standing. Claimed. The site labels the problem OPEN (proof-claims thread of 2026-10-07) and the curator has not commented on either claim. There is no refereed or arXiv version. The audit above is a reading by two named outside persons who later became the formalization's co-authors, and the kernel check is theirs and the authors' report, so this corpus records neither reviewed nor formalized evidence. The problem's standing derives from Wang's claim, accepted on this corpus's build and audit of a port of its Lean proof; this page remains a pending full claim of the same theorem by an independent proof.

Depends on. Nothing in this wiki.