Erdős Problem #1002
OPENdatabase updated 2025-09-07
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
For any \(0<\alpha<1\), let \(f(\alpha,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{ \alpha k\})\). Does \(f(\alpha,n)\) have an asymptotic distribution function? In other words, is there a non-decreasing function \(g\) such that \(g(-\infty)=0\), \(g(\infty)=1\), and \(\lim_{n\to \infty}\lvert \{ \alpha\in (0,1): f(\alpha,n)\leq c\}\rvert=g(c)\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1002.Prizenone
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1002
Attempts
submit one →Read our working report →
The live page is OPEN (accessed 2026-07-31) and shows no current worker, but it lists 2 full proof claims—by Shouqiao Wang (submitted 2026-07-21) and Sangyoon Kwon (submitted 2026-07-23)—so the mandat
SKIPPED