Erdős Problem 997 to Erdős Problem 999
TheoremErdő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)
Quoted from FormalConjectures/ErdosProblems/997.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/997.
The file states 3 research or textbook statements: 3 solved.
Erdos997.erdos_997
Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/pitmonticone/016f2ed66b4cd1c4c4b9998095170e60/raw/b7dfc05c525ae385b5835f89f1ada721443e4305/Erdos997.lean.
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 erdos_997 :
∀ α : ℝ, ¬ IsWellDistributed (fun n ↦ Int.fract (α * (n.nth Nat.Prime)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/997.lean, line 68.
Erdos997.erdos_997.variants.lacunary
Solved: stated here without proof.
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 erdos_997.variants.lacunary (n : ℕ → ℕ) (h : IsLacunary n) :
∀ᵐ α, ¬ IsWellDistributed (fun k ↦ Int.fract (α * (n k : ℝ)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/997.lean, line 77.
Erdos997.erdos_997.variants.irrational
Solved: stated here without proof.
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].
theorem erdos_997.variants.irrational :
∃ α : ℝ, Irrational α ∧
¬ IsWellDistributed (fun n ↦ Int.fract (α * (n.nth Nat.Prime)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/997.lean, line 90.
Sources
TheoremErdős Problem 999#
References: - erdosproblems.com/999 - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65. - [KoMa20] Koukoulopoulos, Dimitris and Maynard, James, On the Duffin-Schaeffer conjecture. Ann. of Math. (2) (2020), 251--307.
Quoted from FormalConjectures/ErdosProblems/999.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/999.
The file states 3 research or textbook statements: 2 solved and 1 textbook result.
Erdos999.erdos_999
Solved: stated here without proof.
For any function \(f:\mathbb{N}\to \mathbb{R}_{\geq 0}\) the property that, for almost all \(\alpha\)
\[\left\lvert \alpha-\frac{p}{q}\right\rvert < \frac{f(q)}{q}\]has infinitely many solutions with \((p,q)=1\), is equivalent to
\[\sum_{q\geq 1}\phi(q)\frac{f(q)}{q}=\infty.\]The Duffin–Schaeffer conjecture. It is easy to prove that the latter follows from the former. Erdős proved this in the special case when \(f(q)q\) is bounded. The full conjecture was proved by Koukoulopoulos and Maynard [KoMa20].
theorem erdos_999 : ∀ f : ℕ → ℝ, (∀ q, 0 ≤ f q) →
((∀ᵐ x : ℝ, IsApproximable f x) ↔
¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/999.lean, line 55.
Erdos999.erdos_999.variants.easy_direction
Textbook result, stated without proof.
It is easy to prove that divergence of the series follows from approximability almost everywhere (the Borel–Cantelli lemma).
theorem erdos_999.variants.easy_direction (f : ℕ → ℝ) (hf : ∀ q, 0 ≤ f q)
(h : ∀ᵐ x : ℝ, IsApproximable f x) :
¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/999.lean, line 63.
Erdos999.erdos_999.variants.erdos
Solved: stated here without proof.
Erdős [Er64b] proved the conjecture in the special case when \(f(q)q\) is bounded.
theorem erdos_999.variants.erdos (f : ℕ → ℝ) (hf : ∀ q, 0 ≤ f q)
(hb : ∃ C : ℝ, ∀ q, f q * q ≤ C) :
(∀ᵐ x : ℝ, IsApproximable f x) ↔
¬ Summable fun q : ℕ ↦ (Nat.totient q : ℝ) * f q / q
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/999.lean, line 70.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.