785.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 10 contain sorry, 0 declared as axioms

Erdős Problem 785

References:

erdosproblems.com/785
[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.

Imports (1)

FormalConjecturesUtil

def Erdos785.counting The counting function $A(x)=\lvert A\cap [1,x]\rvert$ line 53 source
Source documentation
The counting function $A(x)=\lvert A\cap [1,x]\rvert$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, Inter.inter, Set.Icc, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
noncomputable def counting (A : Set ℕ) (x : ℕ) : ℕ :=
…
```
def Erdos785.aStar The 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) line 58 source
Source documentation
The 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).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: SupSet.sSup, Inter.inter, Set.Icc, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
noncomputable def aStar (A : Set ℕ) (x : ℕ) : ℕ :=
…
```
def Erdos785.IsExactAdditiveComplement 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$ line 63 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: And, IsAdditiveComplement, Filter.Tendsto, Real, HDiv.hDiv, HMul.hMul, Erdos785.counting, Filter.atTop, nhds, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
def IsExactAdditiveComplement (A B : Set ℕ) : Prop :=
…
```
theorem Erdos785.erdos_785 sorry line 82 source
depends on sorry what this means
Statement uses: Iff, True, Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Filter.Tendsto, Real, HSub.hSub, HMul.hMul, Erdos785.counting, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos785.erdos_785.variants.danzer Danzer [Da64] proved that exact additive complements exist (Hanani had earlier conjectured they do not exist, as reported in [Er57] and [Er61]) sorry line 92 source
Source documentation
Danzer [Da64] proved that exact additive complements exist (Hanani had earlier conjectured they do not exist, as reported in [Er57] and [Er61]).

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.danzer :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ IsExactAdditiveComplement A B := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement
theorem Erdos785.erdos_785.variants.sarkozy_szemeredi Sárközy and Szemerédi [SaSz94] proved that it is impossible for $$A(x)B(x)-x=o(A(x)).$$ sorry line 101 source
Source documentation
Sárközy and Szemerédi [SaSz94] proved that it is impossible for $$A(x)B(x)-x=o(A(x)).$$

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Asymptotics.IsLittleO, Real, Filter.atTop, HSub.hSub, HMul.hMul, Erdos785.counting
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.sarkozy_szemeredi (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) :
    ¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =o[atTop]
      (fun x : ℕ => (counting A x : ℝ)) := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement, Erdos785.counting
theorem Erdos785.erdos_785.variants.chen_fang Chen and Fang [ChFa15] proved $A(x)B(x)-x\ll \min(A(x),B(x))^c$ cannot hold for any constant $c>0$ sorry line 112 source
Source documentation
Chen and Fang [ChFa15] proved $A(x)B(x)-x\ll \min(A(x),B(x))^c$ cannot hold for any constant $c>0$. In particular $A(x)B(x)-x\ll A(x)^c$ cannot hold when $A$ is the sparser of the two sets.

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Real, LT.lt, Asymptotics.IsBigO, Filter.atTop, HSub.hSub, HMul.hMul, Erdos785.counting, HPow.hPow, Min.min
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.chen_fang (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) (c : ℝ) (hc : 0 < c) :
    ¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =O[atTop]
      (fun x : ℕ => (min (counting A x) (counting B x) : ℝ) ^ c) := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement, c, Erdos785.counting
theorem Erdos785.erdos_785.variants.narkiewicz 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$ sorry line 123 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Or, And, Filter.Tendsto, Real, HDiv.hDiv, Erdos785.counting, HMul.hMul, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.narkiewicz (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (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)) := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement, Erdos785.counting
theorem Erdos785.erdos_785.variants.ruzsa_upper_bound 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$ sorry line 138 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Nat, Real, Filter.Tendsto, Filter.atTop, Exists, Set, And, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Filter.Frequently, LT.lt, HSub.hSub, HMul.hMul, Erdos785.counting
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.ruzsa_upper_bound (w : ℕ → ℝ) (hw : Tendsto w atTop atTop) :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ IsExactAdditiveComplement A B ∧
      ∃ᶠ x : ℕ in atTop, (counting A x * counting B x : ℝ) - (x : ℝ) < w x := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement, Erdos785.counting
theorem Erdos785.erdos_785.variants.ruzsa_lower_bound Documented declaration: ruzsa_lower_bound sorry line 149 source
Source documentation
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)}.$$

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, Erdos785.IsExactAdditiveComplement, Or, Real, GT.gt, Filter.Eventually, LT.lt, HDiv.hDiv, HMul.hMul, HSub.hSub, Erdos785.aStar, Erdos785.counting, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.ruzsa_lower_bound (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (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 : ℝ)) := by
…
```
Mentions: Erdos785.IsExactAdditiveComplement, Erdos785.aStar, Erdos785.counting
theorem Erdos785.erdos_785.variants.chen_fang_limsup Documented declaration: chen_fang_limsup sorry line 166 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, IsAdditiveComplement, LT.lt, EReal, Filter.limsup, HDiv.hDiv, HMul.hMul, Real, Erdos785.counting, Filter.atTop, HSub.hSub, Real.sqrt, Filter.Tendsto
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.chen_fang_limsup (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (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 := by
…
```
Mentions: IsAdditiveComplement, Erdos785.counting
theorem Erdos785.erdos_785.variants.chen_conjecture Chen conjectures that this should be true with $3/2$ sorry line 177 source
Source documentation
Chen conjectures that this should be true with $3/2$.

depends on sorry what this means
Statement uses: Iff, True, Set, Nat, Set.Infinite, Not, Membership.mem, OfNat.ofNat, IsAdditiveComplement, LT.lt, EReal, Filter.limsup, HDiv.hDiv, HMul.hMul, Real, Erdos785.counting, Filter.atTop, Filter.Tendsto, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.chen_conjecture : answer(sorry) ↔
    ∀ A B : Set ℕ, A.Infinite → B.Infinite → 0 ∉ A → 0 ∉ B → 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 := by
…
```
Mentions: IsAdditiveComplement, Erdos785.counting
theorem Erdos785.erdos_785.variants.chen_fang_sharp This is sharp, as Chen and Fang [ChFa11] also proved that there exist such sorry line 190 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, Set.Infinite, Not, Membership.mem, OfNat.ofNat, IsAdditiveComplement, Eq, EReal, Filter.limsup, HDiv.hDiv, HMul.hMul, Real, Erdos785.counting, Filter.atTop, Filter.Frequently, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_785.variants.chen_fang_sharp :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ 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 := by
…
```
Mentions: IsAdditiveComplement, Erdos785.counting