Erdős Problem 32

References:

• erdosproblems.com/32
• [Erd54] Erdős, Paul, Some results on additive number theory. Proc. Amer. Math. Soc. (1954), 847-853.
• [Guy04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437
• [Ru98c] Ruzsa, Imre Z., On the additive completion of primes. Acta Arith. (1998), 269-275.

def Erdos32.IsAdditiveComplementToPrimes (A : Set ℕ) : Prop

A set $A \subseteq \mathbb{N}$ is an additive complement to the primes if every sufficiently large natural number can be written as $p + a$ for some prime $p$ and $a \in A$.

Equations

• Erdos32.IsAdditiveComplementToPrimes A = ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (p : ℕ), Nat.Prime p ∧ ∃ a ∈ A, n = p + a

theorem Erdos32.erdos_32.varaints.log_squared : ∃ (A : Set ℕ), IsAdditiveComplementToPrimes A ∧ (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card) =O[Filter.atTop] fun (N : ℕ) => Real.log ↑N ^ 2

Erdős proved in [Erd54] that there exists an additive complement $A$ to the primes with $|A \cap \{1, \ldots, N\}| = O((\log N)^2)$.

theorem Erdos32.erdos_32.variants.liminf_gt_one (A : Set ℕ) : IsAdditiveComplementToPrimes A → 1 < Filter.liminf (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card / ↑(Real.log ↑N)) Filter.atTop

Must every additive complement $A$ to the primes satisfy $\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} > 1$?

theorem Erdos32.erdos_32 : sorry ↔ ∃ (A : Set ℕ), IsAdditiveComplementToPrimes A ∧ (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card) =o[Filter.atTop] fun (N : ℕ) => Real.log ↑N ^ 2

Does there exist a set $A \subseteq \mathbb{N}$ such that $|A \cap \{1, \ldots, N\}| = o((\log N)^2)$ and every sufficiently large integer can be written as $p + a$ for some prime $p$ and $a \in A$?

theorem Erdos32.erdos_32.variants.log_bound : sorry ↔ ∃ (A : Set ℕ), IsAdditiveComplementToPrimes A ∧ (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card) =O[Filter.atTop] fun (N : ℕ) => Real.log ↑N

Can the bound $O(\log N)$ be achieved for an additive complement to the primes? [Guy04] writes that Erdős offered $50 for the solution.

theorem Erdos32.erdos_32.variants.ruzsa (A : Set ℕ) : IsAdditiveComplementToPrimes A → ↑(Real.exp Real.eulerMascheroniConstant) ≤ Filter.liminf (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card / ↑(Real.log ↑N)) Filter.atTop

Ruzsa proved that any additive complement $A$ to the primes must satisfy $\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} \geq e^\gamma$, where $\gamma$ is the Euler-Mascheroni constant.