/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilErdős Problem 1000
References:
[Ca50b] Cassels, J. W. S., Some metrical theorems in Diophantine approximation. I. Proc. Cambridge Philos. Soc. (1950), 209-218.
[Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65.
[Ha] Haight, J. A., Metric Diophantine approximation and related topics. PhD thesis.
@[expose] public sectionopen Filter Topologynamespace Erdos1000
Given an infinite sequence of positive integers $A = {n_1 < n_2 < \cdots}$, phiSeq n k is
$\phi_A(k)$: the number of $1\leq m\leq n_k$ such that $\frac{m}{n_k}$ cannot be written as
$\frac{b}{n_j}$ for any integer $b$ and any $1\leq j<k$; equivalently,
$$
\frac{n_k}{(m,n_k)}\nmid n_j
$$
for all $1\leq j<k$.
def phiSeq (n : ℕ → ℕ) (k : ℕ) : ℕ :=
((Finset.Icc 1 (n k)).filter fun m => ∀ j < k, ¬ (n k / Nat.gcd m (n k)) ∣ n j).cardThe average $\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}$.
noncomputable def phiAvg (n : ℕ → ℕ) (N : ℕ) : ℝ :=
(∑ k ∈ Finset.range N, (phiSeq n k : ℝ) / (n k : ℝ)) / (N : ℝ)Let $A={n_1<n_2<\cdots}$ be an infinite sequence of positive integers, and let $\phi_A(k)$ count the number of $1\leq m\leq n_k$ such that the fraction $\frac{m}{n_k}$ cannot be written as $\frac{b}{n_j}$ for any integer $b$ and any $j<k$; equivalently, $$ \frac{n_k}{(m,n_k)}\nmid n_j $$ for all $1\leq j<k$.
Is there a sequence $A$ such that $$ \lim_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0? $$
This was solved by Haight [Ha] who proved that such a sequence does exist (contrary to Erdős' expectations).
@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1000.lean"]
theorem erdos_1000 : answer(True) ↔
∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
Tendsto (phiAvg n) atTop (𝓝 0) := ⊢ True ↔ ∃ n, StrictMono n ∧ 0 < n 0 ∧ Tendsto (phiAvg n) atTop (𝓝 0)
All goals completed! 🐙It is trivial that $\phi_A(k)\geq \phi(n_k)$, where $\phi$ is the Euler totient function.
n:ℕ → ℕhn:StrictMono nhn0:0 < n 0k:ℕa:ℕb:ℕhab:(if a = 0 then n k else a) = if b = 0 then n k else bha:a < n k ∧ (n k).Coprime ahb:b < n k ∧ (n k).Coprime bh1:¬a = 0h2:b = 0this:n k = 1⊢ a = b
All goals completed! 🐙
n:ℕ → ℕhn:StrictMono nhn0:0 < n 0k:ℕa:ℕb:ℕhab:(if a = 0 then n k else a) = if b = 0 then n k else bha:a < n k ∧ (n k).Coprime ahb:b < n k ∧ (n k).Coprime bh1:¬a = 0h2:¬b = 0⊢ a = b All goals completed! 🐙The study of $\phi_A$ was introduced by Cassels [Ca50b], who proved that there exist sequences such that $$ \liminf_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0. $$
@[category research solved, AMS 11]
theorem erdos_1000.variants.liminf_eq_zero :
∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
atTop.liminf (phiAvg n) = 0 := ⊢ ∃ n, StrictMono n ∧ 0 < n 0 ∧ liminf (phiAvg n) atTop = 0
All goals completed! 🐙Erdős [Er64b] proved that the limit of $\frac{\phi_A(k)}{n_k}$ as $k\to \infty$ cannot be $0$.
@[category research solved, AMS 11]
theorem erdos_1000.variants.not_tendsto_zero (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0) :
¬ Tendsto (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) atTop (𝓝 0) := n:ℕ → ℕhn:StrictMono nhn0:0 < n 0⊢ ¬Tendsto (fun k ↦ ↑(phiSeq n k) / ↑(n k)) atTop (𝓝 0)
All goals completed! 🐙In fact he proved that if $\liminf \frac{\phi_A(k)}{n_k}=0$ then $\limsup \frac{\phi_A(k)}{n_k}=1$.
@[category research solved, AMS 11]
theorem erdos_1000.variants.limsup_eq_one (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0)
(h : atTop.liminf (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 0) :
atTop.limsup (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 1 := n:ℕ → ℕhn:StrictMono nhn0:0 < n 0h:liminf (fun k ↦ ↑(phiSeq n k) / ↑(n k)) atTop = 0⊢ limsup (fun k ↦ ↑(phiSeq n k) / ↑(n k)) atTop = 1
All goals completed! 🐙end Erdos1000