Ben Green's Open Problem 46

What is the largest $y$ for which one may cover the interval $[y]$ by residue classes $a_p \pmod{p}$, one for each prime $p \leq x$?

References:

• [Gr24] Ben Green's Open Problem 46
• [FGK18] Ford, K., Green, B., Konyagin, S., Maynard, J., & Tao, T. (2018). Long gaps between primes. Journal of the American Mathematical Society, 31(1), 65-105.
• [Iw78] Iwaniec, Henryk. "On the problem of Jacobsthal." Demonstratio Mathematica 11.1 (1978): 225-232.

def Green46.IsCoveredByResidues (x y : ℕ) : Prop

Given $x$ and $y$, can we cover the interval $[1, y]$ by residue classes $a_p \pmod p$ for each prime $p \le x$?

Equations

• Green46.IsCoveredByResidues x y = ∃ (a : ℕ → ℕ), ∀ m ∈ Finset.Icc 1 y, ∃ p ≤ x, Nat.Prime p ∧ m ≡ a p [MOD p]

noncomputable def Green46.maxY (x : ℕ) : ℝ

The maximum $y$ for a given $x$, cast to a real number for asymptotics.

Equations

• Green46.maxY x = ↑(sSup {y : ℕ | Green46.IsCoveredByResidues x y})

noncomputable def Green46.bestLower (x : ℕ) : ℝ

Best-known lower bound [Ra38].

Equations

• Green46.bestLower x = ↑x * Real.log ↑x * Real.log (Real.log (Real.log ↑x)) / Real.log (Real.log ↑x)

noncomputable def Green46.bestUpper (x : ℕ) : ℝ

Best-known upper bound [Iw78].

Equations

• Green46.bestUpper x = ↑x ^ 2

theorem Green46.green_46.improve_lower : have ans := sorry; bestLower =o[Filter.atTop] ans ∧ ans =O[Filter.atTop] maxY

We conjecture that the best-known lower bound can be improved.

theorem Green46.green_46.improve_upper : have ans := sorry; ans =o[Filter.atTop] bestUpper ∧ maxY =O[Filter.atTop] ans

We conjecture that the best-known upper bound can be improved.

theorem Green46.green_46.improve_upper_conjectured : ∃ (o : ℕ → ℝ), (o =o[Filter.atTop] fun (x : ℕ) => 1) ∧ maxY =O[Filter.atTop] fun (x : ℕ) => ↑x ^ (1 + o x)

It seems very likely that we must have $y \ll x^{1+o(1)}$ [Gr24].

theorem Green46.green_46.variants.lower : bestLower =O[Filter.atTop] maxY

Best known lower bound: $y \gg x \frac{\log x \log \log \log x}{\log \log x}$ [Ra38].

theorem Green46.green_46.variants.upper : maxY =O[Filter.atTop] bestUpper

Best known upper bound: $y \ll x^2$ [Iw78].