/-
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.
-/
import FormalConjecturesUtilErdős Problem 950
[Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.
open Filteropen scoped Asymptotics Nat.Prime
namespace Erdos950
Let $f(n) = \sum_{p<n}\frac{1}{n-p}$.
noncomputable def f (n : ℕ) : ℝ :=
∑ p ∈ (Finset.range n).filter Prime, (1 : ℝ) / (n - p : ℝ)
Is it true that $\liminf f(n)=1$?
@[category research open, AMS 11]
theorem erdos_950.parts.i :
answer(sorry) ↔ atTop.liminf (fun n : ℕ ↦ (f n : EReal)) = 1 := ⊢ True ↔ liminf (fun n => ↑(f n)) atTop = 1
All goals completed! 🐙
Is it true that $\limsup f(n)=\infty$?
@[category research open, AMS 11]
theorem erdos_950.parts.ii :
answer(sorry) ↔ atTop.limsup (fun n : ℕ ↦ (f n : EReal)) = ⊤ := ⊢ True ↔ limsup (fun n => ↑(f n)) atTop = ⊤
All goals completed! 🐙
Is it true that $f(n)=o(\log\log n)$ for all $n$?
@[category research open, AMS 11]
theorem erdos_950.parts.iii :
answer(sorry) ↔ f =o[atTop] (fun n : ℕ ↦ Real.log (Real.log n)) := ⊢ True ↔ f =o[atTop] fun n => Real.log (Real.log ↑n)
All goals completed! 🐙
This function was considered by de Bruijn, Erdős, and Turán, who showed that $\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x$. They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].
@[category research solved, AMS 11]
theorem erdos_950.variants.debruijn_erdos_turan :
(fun x : ℕ ↦ ∑ n ∈ Finset.range x, f n) ~[atTop] (fun x : ℕ ↦ (x : ℝ)) ∧
(fun x : ℕ ↦ ∑ n ∈ Finset.range x, (f n) ^ 2) ~[atTop] (fun x : ℕ ↦ (x : ℝ)) := ⊢ ((fun x => ∑ n ∈ Finset.range x, f n) ~[atTop] fun x => ↑x) ∧
(fun x => ∑ n ∈ Finset.range x, f n ^ 2) ~[atTop] fun x => ↑x
All goals completed! 🐙
Erdős writes that a 'weaker conjecture which is perhaps not quite inaccessible' is that, for every $\epsilon>0$, if $x$ is sufficiently large there exists $y<x$ such that $\pi(x)< \pi(y)+\epsilon \pi(x-y)$. Compare this to [855].
@[category research open, AMS 11]
theorem erdos_950.variants.weaker_pi :
answer(sorry) ↔ ∀ ε > 0, ∀ᶠ x in atTop, ∃ y < x,
(π x : ℝ) < (π y : ℝ) + ε * (π (x - y) : ℝ) := ⊢ True ↔ ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, ∃ y < x, ↑(π x) < ↑(π y) + ε * ↑(π (x - y))
All goals completed! 🐙
He notes that if $\pi(x)< \pi(y)+O\left(\frac{x-y}{\log x}\right)$ for all $y<x-(\log x)^C$ for some constant $C>0$ then $f(n)\ll \log\log\log n$.
@[category research solved, AMS 11]
theorem erdos_950.variants.weaker_pi_implies_f
(h : ∃ C > (0 : ℝ), ∃ K > (0 : ℝ), ∀ᶠ x : ℕ in atTop, ∀ y : ℕ,
(y : ℝ) < x - (Real.log x) ^ C →
(π x : ℝ) < (π y : ℝ) + K * ((x - y : ℝ) / Real.log x)) :
f =O[atTop] fun n : ℕ ↦ Real.log (Real.log (Real.log n)) := h:∃ C > 0,
∃ K > 0, ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), ↑y < ↑x - Real.log ↑x ^ C → ↑(π x) < ↑(π y) + K * ((↑x - ↑y) / Real.log ↑x)⊢ f =O[atTop] fun n => Real.log (Real.log (Real.log ↑n))
All goals completed! 🐙
The study of $f(p)$ is even harder, and Erdős could not prove that $\sum_{p<x}f(p)^2\sim \pi(x)$.
@[category research open, AMS 11]
theorem erdos_950.variants.sum_primes :
answer(sorry) ↔
(fun x : ℕ ↦ ∑ p ∈ (Finset.range x).filter Prime, (f p) ^ 2) ~[atTop]
fun x ↦ (π x : ℝ) := ⊢ True ↔ (fun x => ∑ p ∈ Finset.range x with Prime p, f p ^ 2) ~[atTop] fun x => ↑(π x)
All goals completed! 🐙
end Erdos950