/-
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 785
References:
[ChFa10] Fang, Jin-Hui and Chen, Yong-Gao, On additive complements. Proc. Amer. Math. Soc. (2010), 1923-1927.
[ChFa11] Chen, Yong-Gao and Fang, Jin-Hui, On additive complements. II. Proc. Amer. Math. Soc. (2011), 881-883.
[ChFa14] Fang, Jin-Hui and Chen, Yong-Gao, On additive complements. III. J. Number Theory (2014), 83-91.
[ChFa15] Chen, Yong-Gao and Fang, Jin-Hui, On a conjecture of Sárközy and Szemerédi. Acta Arith. (2015), 47-58.
[Da64] Danzer, L., Über eine Frage von G. Hanani aus der additiven Zahlentheorie. J. Reine Angew. Math. (1964), 392-394.
[Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300.
[Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
[Na59] Narkiewicz, Władysław, Remarks on a conjecture of Hanani in additive number theory. Colloq. Math. (1959/60), 161-165.
[Ru17] Ruzsa, Imre Z., Exact additive complements. Q. J. Math. (2017), 227-235.
[SaSz94] Sárközy, A. and Szemerédi, E., On a problem in additive number theory. Acta Math. Hungar. (1994), 237-245.
open Filter Pointwiseopen scoped Topologynamespace Erdos785The counting function $A(x)=\lvert A\cap [1,x]\rvert$.
noncomputable def counting (A : Set ℕ) (x : ℕ) : ℕ :=
(A ∩ Set.Icc 1 x).ncardThe largest element of $A$ in $[1,x]$, that is $a^*(x)=\max A\cap [1,x]$ (equal to $0$ when there is no such element).
noncomputable def aStar (A : Set ℕ) (x : ℕ) : ℕ :=
sSup (A ∩ Set.Icc 1 x)Two sets $A, B\subseteq \mathbb{N}$ are exact additive complements if $A+B$ contains all large integers and $A(x)B(x)\sim x$.
def IsExactAdditiveComplement (A B : Set ℕ) : Prop :=
IsAdditiveComplement A B ∧
Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) / (x : ℝ)) atTop (𝓝 1)Let $A,B\subseteq \mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\lvert A\cap [1,x]\rvert$ and similarly for $B(x)$. Is it true that if $A(x)B(x)\sim x$ then $$A(x)B(x)-x\to \infty$$ as $x\to \infty$?
A conjecture of Erdős and Danzer. The answer is yes, proved by Sárközy and Szemerédi [SaSz94], who actually proved that it is impossible for $$A(x)B(x)-x=o(A(x)).$$
This was formalized in Lean by van Doorn using Aristotle.
@[category research solved, AMS 11, formal_proof using lean4 at
"https://github.com/Woett/Lean-files/blob/main/ErdosProblem785.lean"]
theorem erdos_785 : answer(True) ↔
∀ A B : Set ℕ, A.Infinite → B.Infinite → IsExactAdditiveComplement A B →
Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop := ⊢ True ↔
∀ (A B : Set ℕ),
A.Infinite →
B.Infinite → IsExactAdditiveComplement A B → Tendsto (fun x ↦ ↑(counting A x) * ↑(counting B x) - ↑x) atTop atTop
All goals completed! 🐙Danzer [Da64] proved that exact additive complements exist (Hanani had earlier conjectured they do not exist, as reported in [Er57] and [Er61]).
@[category research solved, AMS 11]
theorem erdos_785.variants.danzer :
∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ IsExactAdditiveComplement A B := ⊢ ∃ A B, A.Infinite ∧ B.Infinite ∧ IsExactAdditiveComplement A B
All goals completed! 🐙Sárközy and Szemerédi [SaSz94] proved that it is impossible for $$A(x)B(x)-x=o(A(x)).$$
@[category research solved, AMS 11]
theorem erdos_785.variants.sarkozy_szemeredi (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
(h : IsExactAdditiveComplement A B) :
¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =o[atTop]
(fun x : ℕ => (counting A x : ℝ)) := A:Set ℕB:Set ℕhA:A.InfinitehB:B.Infiniteh:IsExactAdditiveComplement A B⊢ ¬(fun x ↦ ↑(counting A x) * ↑(counting B x) - ↑x) =o[atTop] fun x ↦ ↑(counting A x)
All goals completed! 🐙Chen and Fang [ChFa15] proved $A(x)B(x)-x\ll A(x)^c$ cannot hold for any constant $c>0$.
@[category research solved, AMS 11]
theorem erdos_785.variants.chen_fang (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
(h : IsExactAdditiveComplement A B) (c : ℝ) (hc : 0 < c) :
¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =O[atTop]
(fun x : ℕ => (counting A x : ℝ) ^ c) := A:Set ℕB:Set ℕhA:A.InfinitehB:B.Infiniteh:IsExactAdditiveComplement A Bc:ℝhc:0 < c⊢ ¬(fun x ↦ ↑(counting A x) * ↑(counting B x) - ↑x) =O[atTop] fun x ↦ ↑(counting A x) ^ c
All goals completed! 🐙Narkiewicz [Na59] proved that, under the given assumptions (and perhaps swapping $A$ and $B$) we must have $A(2x)/A(x)\to 1$ and $B(2x)/B(x)\to 2$.
@[category research solved, AMS 11]
theorem erdos_785.variants.narkiewicz (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
(h : IsExactAdditiveComplement A B) :
(Tendsto (fun x : ℕ => (counting A (2 * x) : ℝ) / (counting A x : ℝ)) atTop (𝓝 1) ∧
Tendsto (fun x : ℕ => (counting B (2 * x) : ℝ) / (counting B x : ℝ)) atTop (𝓝 2)) ∨
(Tendsto (fun x : ℕ => (counting B (2 * x) : ℝ) / (counting B x : ℝ)) atTop (𝓝 1) ∧
Tendsto (fun x : ℕ => (counting A (2 * x) : ℝ) / (counting A x : ℝ))
atTop (𝓝 2)) := A:Set ℕB:Set ℕhA:A.InfinitehB:B.Infiniteh:IsExactAdditiveComplement A B⊢ Tendsto (fun x ↦ ↑(counting A (2 * x)) / ↑(counting A x)) atTop (𝓝 1) ∧
Tendsto (fun x ↦ ↑(counting B (2 * x)) / ↑(counting B x)) atTop (𝓝 2) ∨
Tendsto (fun x ↦ ↑(counting B (2 * x)) / ↑(counting B x)) atTop (𝓝 1) ∧
Tendsto (fun x ↦ ↑(counting A (2 * x)) / ↑(counting A x)) atTop (𝓝 2)
All goals completed! 🐙Ruzsa [Ru17] has constructed, for any function $w(x)\to \infty$, such a pair of sets with $$A(x)B(x)-x<w(x)$$ for infinitely many $x$.
@[category research solved, AMS 11]
theorem erdos_785.variants.ruzsa_upper_bound (w : ℕ → ℝ) (hw : Tendsto w atTop atTop) :
∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ IsExactAdditiveComplement A B ∧
∃ᶠ x : ℕ in atTop, (counting A x * counting B x : ℝ) - (x : ℝ) < w x := w:ℕ → ℝhw:Tendsto w atTop atTop⊢ ∃ A B,
A.Infinite ∧
B.Infinite ∧ IsExactAdditiveComplement A B ∧ ∃ᶠ (x : ℕ) in atTop, ↑(counting A x) * ↑(counting B x) - ↑x < w x
All goals completed! 🐙Ruzsa [Ru17] proves that, if $a^(x)=\max A \cap [1,x]$ and $A$ and $B$ satisfy the conditions in the problem then (after possibly changing the roles of $A$ and $B$) $$A(x)B(x)-x > (1-o(1))\frac{a^(x)}{A(x)}.$$
@[category research solved, AMS 11]
theorem erdos_785.variants.ruzsa_lower_bound (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
(h : IsExactAdditiveComplement A B) :
(∀ ε > (0 : ℝ), ∀ᶠ x : ℕ in atTop,
(1 - ε) * (aStar A x : ℝ) / (counting A x : ℝ)
< (counting A x * counting B x : ℝ) - (x : ℝ)) ∨
(∀ ε > (0 : ℝ), ∀ᶠ x : ℕ in atTop,
(1 - ε) * (aStar B x : ℝ) / (counting B x : ℝ)
< (counting A x * counting B x : ℝ) - (x : ℝ)) := A:Set ℕB:Set ℕhA:A.InfinitehB:B.Infiniteh:IsExactAdditiveComplement A B⊢ (∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, (1 - ε) * ↑(aStar A x) / ↑(counting A x) < ↑(counting A x) * ↑(counting B x) - ↑x) ∨
∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, (1 - ε) * ↑(aStar B x) / ↑(counting B x) < ↑(counting A x) * ↑(counting B x) - ↑x
All goals completed! 🐙Chen and Fang [ChFa10] proved the stronger statement that $A(x)B(x)-x\to \infty$ if $A$ and $B$ are infinite sets such that $A+B$ contains all large integers and $$\limsup_{x\to \infty}\frac{A(x)B(x)}{x}<\frac{5}{4}.$$ They later [ChFa14] improved $5/4$ to $3-\sqrt{3}\approx 1.268$.
@[category research solved, AMS 11]
theorem erdos_785.variants.chen_fang_limsup (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
(h : IsAdditiveComplement A B)
(hlim : limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
< ((3 - Real.sqrt 3 : ℝ) : EReal)) :
Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop := A:Set ℕB:Set ℕhA:A.InfinitehB:B.Infiniteh:IsAdditiveComplement A Bhlim:limsup (fun x ↦ ↑(↑(counting A x) * ↑(counting B x)) / ↑↑x) atTop < ↑(3 - √3)⊢ Tendsto (fun x ↦ ↑(counting A x) * ↑(counting B x) - ↑x) atTop atTop
All goals completed! 🐙Chen conjectures that this should be true with $3/2$.
@[category research open, AMS 11]
theorem erdos_785.variants.chen_conjecture : answer(sorry) ↔
∀ A B : Set ℕ, A.Infinite → B.Infinite → IsAdditiveComplement A B →
limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
< ((3 / 2 : ℝ) : EReal) →
Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop := ⊢ True ↔
∀ (A B : Set ℕ),
A.Infinite →
B.Infinite →
IsAdditiveComplement A B →
limsup (fun x ↦ ↑(↑(counting A x) * ↑(counting B x)) / ↑↑x) atTop < ↑(3 / 2) →
Tendsto (fun x ↦ ↑(counting A x) * ↑(counting B x) - ↑x) atTop atTop
All goals completed! 🐙This is sharp, as Chen and Fang [ChFa11] also proved that there exist such $A$ and $B$ with $$\limsup_{x\to \infty}\frac{A(x)B(x)}{x}=\frac{3}{2}$$ for which $A(x)B(x)-x=1$ for infinitely many $x$.
@[category research solved, AMS 11]
theorem erdos_785.variants.chen_fang_sharp :
∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ IsAdditiveComplement A B ∧
limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
= ((3 / 2 : ℝ) : EReal) ∧
∃ᶠ x : ℕ in atTop, (counting A x * counting B x : ℝ) - (x : ℝ) = 1 := ⊢ ∃ A B,
A.Infinite ∧
B.Infinite ∧
IsAdditiveComplement A B ∧
limsup (fun x ↦ ↑(↑(counting A x) * ↑(counting B x)) / ↑↑x) atTop = ↑(3 / 2) ∧
∃ᶠ (x : ℕ) in atTop, ↑(counting A x) * ↑(counting B x) - ↑x = 1
All goals completed! 🐙end Erdos785