Erdős Problem 997

References:

• erdosproblems.com/997
• [APSSV26] B. Alexeev, M. Putterman, M. Sawhney, M. Sellke, and G. Valiant, Short proofs in combinatorics and number theory. arXiv:2603.29961 (2026).
• [CLLW24] J. Champagne, T. Le, Y.-R. Liu, and T. D. Wooley, Well-distribution modulo one and the primes. arXiv:2406.19491 (2024).
• [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65.
• [Er85e] Erdős, P., Some problems and results in number theory. Number theory and combinatorics. Japan 1984 (Tokyo, Okayama and Kyoto, 1984) (1985), 65-87.
• [Hl55] Hlawka, Edmund, Zur formalen {T}heorie der {G}leichverteilung in kompakten {G}ruppen. Rend. Circ. Mat. Palermo (2) (1955), 33--47.
• [Mo26] P. Monticone, Lean formalisation of Erdős problem 997 (2026)

def Erdos997.IsWellDistributed (x : ℕ → ℝ) : Prop

Call $x_1,x_2,\ldots \in (0,1)$ well-distributed if, for every $\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\subseteq [0,1]$, $\lvert \# \{ n < m\leq n+k : x_m\in I\} - \lvert I\rvert k\rvert < \epsilon k.$

The notion of a well-distributed sequence was introduced by Hlawka and Petersen [Hl55].

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos997.erdos_997 : True ↔ ∀ (α : ℝ), ¬IsWellDistributed fun (n : ℕ) => Int.fract (α * ↑(Nat.nth Nat.Prime n))

Is it true that, for every $\alpha$, the sequence $\{ \alpha p_n\}$ is not well-distributed, if $p_n$ is the sequence of primes?

The answer is yes, by [APSSV26, Section 4]; a Lean formalisation is available in [Mo26].

theorem Erdos997.erdos_997.variants.lacunary (n : ℕ → ℕ) (h : IsLacunary n) : ∀ᵐ (α : ℝ), ¬IsWellDistributed fun (k : ℕ) => Int.fract (α * ↑(n k))

Erdős proved that, if $n_k$ is a lacunary sequence, then the sequence $\{ \alpha n_k\}$ is not well-distributed for almost all $\alpha$.

theorem Erdos997.erdos_997.variants.irrational : ∃ (α : ℝ), Irrational α ∧ ¬IsWellDistributed fun (n : ℕ) => Int.fract (α * ↑(Nat.nth Nat.Prime n))

He also claimed in [Er64b] to have proved that there exists an irrational $\alpha$ for which $\{\alpha p_n\}$ is not well-distributed. He later retracted this claim in [Er85e], saying "The theorem is no doubt correct and perhaps will not be difficult to prove but I never was able to reconstruct my 'proof' which perhaps never existed."

The existence of such an $\alpha$ was established by Champagne, Le, Liu, and Wooley [CLLW24].