1. FormalConjectures
  2. ErdosProblems
  3. «1145»
/- 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 FormalConjecturesUtil import FormalConjectures.ErdosProblems.«28»

Erdős Problem 1145

References:

open Set Filter Pointwise Topology AdditiveCombinatorics namespace Erdos1145

Let $A={1\leq a_1 < a_2 < \cdots}$ and $B={1\leq b_1 < b_2 < \cdots}$ be sets of integers with $a_n/b_n\to 1$.

If $A+B$ contains all sufficiently large positive integers then is it true that $\limsup 1_A\ast 1_B(n)=\infty$?

Formalization note: There's some discussion in the comments of [erdosproblems.com/28] and [erdosproblems.com/1145] about whether or not $0$ should be included in $A$ or $B$ and has been left purposely ambiguous. Problem 1145 was originally written as $A + B = \mathbb{N}$, which would imply that $0$ would need to exist in $A$ or $B$ to include $1$ in $A + B$. However, it's been made more general and rewritten as "sufficiently large positive integers". The formalization below is the version that includes $0$.

def Erdos1145Prop : Prop := ∀ ⦃A B : Set ℕ⦄ (_ : A.Infinite) (_ : B.Infinite), Tendsto (fun n ↦ (Nat.nth (· ∈ A) n : ℝ) / (Nat.nth (· ∈ B) n : ℝ)) atTop (𝓝 1) → (∀ᶠ n in atTop, n ∈ A + B) → limsup (fun n => ↑(((𝟙_A ∗ 𝟙_B) : ℕ → ℕ) n)) atTop = (⊤ : ℕ∞)

Let $A={1\leq a_1 < a_2 < \cdots}$ and $B={1\leq b_1 < b_2 < \cdots}$ be sets of integers with $a_n/b_n\to 1$.

If $A+B$ contains all sufficiently large positive integers then is it true that $\limsup 1_A\ast 1_B(n)=\infty$?

A conjecture of Erdős and Sárközy.

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_1145 : answer(sorry) ↔ Erdos1145Prop := ⊢ True ↔ Erdos1145Prop All goals completed! 🐙

A stronger form of [erdosproblems.com/28].

@[category test, AMS 11] theorem erdos_1145.test_implies_erdos_28 : Erdos1145Prop → type_of% Erdos28.erdos_28 := ⊢ Erdos1145Prop → ∀ (A : Set ℕ), (A + A)ᶜ.Finite → limsup (fun n => ↑(sumRep A n)) atTop = ⊤ ⊢ Erdos1145Prop → ∀ (A : Set ℕ), (A + A)ᶜ.Finite → limsup (fun n => ↑((𝟙_A ∗ 𝟙_A) n)) atTop = ⊤ intro h1145 h1145:Erdos1145Props:Set ℕ⊢ (s + s)ᶜ.Finite → limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finite⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ m⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:s.Finite⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finite⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:s.Finite⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ All goals completed! 🐙 h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finite⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ limsup (fun n => ↑((𝟙_s ∗ 𝟙_s) n)) atTop = ⊤ h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ Tendsto (fun n => ↑(Nat.nth (fun x => x ∈ s) n) / ↑(Nat.nth (fun x => x ∈ s) n)) atTop (𝓝 1)h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ ∀ᶠ (n : ℕ) in atTop, n ∈ s + s h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ Tendsto (fun n => ↑(Nat.nth (fun x => x ∈ s) n) / ↑(Nat.nth (fun x => x ∈ s) n)) atTop (𝓝 1) h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ (fun x => 1) =ᶠ[atTop] fun n => ↑(Nat.nth (fun x => x ∈ s) n) / ↑(Nat.nth (fun x => x ∈ s) n) filter_upwards [Filter.eventually_gt_atTop 0] with n h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfinn:ℕhn:0 < n⊢ 1 = ↑(Nat.nth (fun x => x ∈ s) n) / ↑(Nat.nth (fun x => x ∈ s) n) h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfinn:ℕhn:0 < n⊢ ↑(Nat.nth (fun x => x ∈ s) n) ≠ 0 All goals completed! 🐙 h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfin⊢ ∀ᶠ (n : ℕ) in atTop, n ∈ s + s filter_upwards [Filter.eventually_gt_atTop m] with n h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfinn:ℕhn:m < n⊢ n ∈ s + s h1145:Erdos1145Props:Set ℕhs:(s + s)ᶜ.Finitem:ℕhm:∀ i ∈ (s + s)ᶜ, i ≤ mhfin:¬s.Finitehinf:s.Infinite := hfinn:ℕhn:m < nhns:n ∉ s + s⊢ False All goals completed! 🐙 end Erdos1145