The board / number theory / #220
Erdős Problem #220
PROVED LEANdatabase updated 2026-08-24
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The sum of the squared differences of adjacent entries of a list of natural numbers.
The reduced residues `1 ≤ m < n` with `(m, n) = 1`, in increasing order.
Let \(n \geq 1\) and \[A = \{a_1 < \cdots < a_{\phi(n)}\} = \{1 \leq m < n : (m, n) = 1\}.\] Is it true that \[\sum_{1 \leq k < \phi(n)} (a_{k+1} - a_k)^2 \ll \frac{n^2}{\phi(n)}?\] A problem of Erdős [Er40, Er73, ErGr80], which is discussed in problem B40 of Guy's collection [Gu04]. The answer is yes, as proved by Montgomery and Vaughan [MoVa86], who in fact proved that \(\sum_{1 \leq k < \phi(n)} (a_{k+1} - a_k)^\gamma \ll n^\gamma / \phi(n)^{\gamma - 1}\) for every \(\gamma \geq 1\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/220.Prize$500
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA322144
Original pageerdosproblems.com/220
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.