1109.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

7 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 1109

References:

erdosproblems.com/1109
[ErSa87] P. Erdős and A. Sárközy, On divisibility properties of integers of the form $a+a'$, Acta Math. Hungar. (1987), 117--122.
[Gy01] Katalin Gyarmati, On divisibility properties of integers of the form $ab+1$, Period. Math. Hungar. (2001), 71--79.
[Ko04] S. V. Konyagin, Problems of the set of square-free numbers, Izv. Ross. Akad. Nauk Ser. Mat. (2004), 63--90.
[Sa92c] G. N. Sárközy, On a problem of P. Erdős, Acta Math. Hungar. (1992), 271--282.

Imports (1)

FormalConjecturesUtil

def Erdos1109.f f N is the largest size of a subset A ⊆ {1, ..., N} such that every element of A + A is squarefree line 46 source
Source documentation
f N is the largest size of a subset A ⊆ {1, ..., N} such that every element of A + A is squarefree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, OfNat.ofNat, Membership.mem, HAdd.hAdd, Squarefree, Eq, Finset.card
14 instances, coercions and auxiliary constants left out.
```
noncomputable def f (N : ℕ) : ℕ :=
…
```
theorem Erdos1109.erdos_1109 Let $f(N)$ be the size of the largest subset $A\subseteq \{1,\ldots,N\}$ such that every $n\in A+A$ is squarefree sorry line 58 source
Source documentation
Let $f(N)$ be the size of the largest subset $A\subseteq \{1,\ldots,N\}$ such that every $n\in A+A$ is squarefree. Estimate $f(N)$. In particular, is it true that $f(N)\leq N^{o(1)}$, or even $f(N) \leq (\log N)^{O(1)}$?
This theorem formalizes the subpolynomial bound as f(N) = O(N^ε) for every ε > 0.

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, Erdos1109.f, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1109 :
    answer(sorry) ↔ ∀ ε > (0 : ℝ),
      (fun N : ℕ => (f N : ℝ)) ≪ fun N : ℕ => (N : ℝ) ^ ε := by
…
```
Mentions: Erdos1109.f
theorem Erdos1109.erdos_1109.variants.polylog Is the stronger polylogarithmic bound $f(N) \leq (\log N)^{O(1)}$ true? sorry line 67 source
Source documentation
Is the stronger polylogarithmic bound $f(N) \leq (\log N)^{O(1)}$ true?

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, Erdos1109.f, HPow.hPow, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1109.variants.polylog :
    answer(sorry) ↔ ∃ C > (0 : ℝ),
      (fun N : ℕ => (f N : ℝ)) ≪ fun N : ℕ => (Real.log N) ^ C := by
…
```
Mentions: Erdos1109.f
theorem Erdos1109.erdos_1109.variants.erdos_sarkozy_lower Erdős and Sárközy [ErSa87] proved the lower bound $\log N \ll f(N)$ sorry line 76 source
Source documentation
Erdős and Sárközy [ErSa87] proved the lower bound $\log N \ll f(N)$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Real.log, Erdos1109.f
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1109.variants.erdos_sarkozy_lower :
    (fun N : ℕ => Real.log N) ≪ fun N : ℕ => (f N : ℝ) := by
…
```
Mentions: Erdos1109.f
theorem Erdos1109.erdos_1109.variants.erdos_sarkozy_upper Erdős and Sárközy [ErSa87] proved the upper bound $f(N) \ll N^{3/4}\log N$ sorry line 84 source
Source documentation
Erdős and Sárközy [ErSa87] proved the upper bound $f(N) \ll N^{3/4}\log N$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos1109.f, HMul.hMul, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1109.variants.erdos_sarkozy_upper :
    (fun N : ℕ => (f N : ℝ)) ≪
      fun N : ℕ => (N : ℝ) ^ ((3 : ℝ) / 4) * Real.log N := by
…
```
Mentions: Erdos1109.f
theorem Erdos1109.erdos_1109.variants.konyagin_lower Konyagin [Ko04] improved the lower bound to $\log\log N(\log N)^2 \ll f(N)$ sorry line 94 source
Source documentation
Konyagin [Ko04] improved the lower bound to $\log\log N(\log N)^2 \ll f(N)$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HMul.hMul, Real.log, HPow.hPow, OfNat.ofNat, Erdos1109.f
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_1109.variants.konyagin_lower :
    (fun N : ℕ => Real.log (Real.log N) * (Real.log N) ^ 2) ≪
      fun N : ℕ => (f N : ℝ) := by
…
```
Mentions: Erdos1109.f
theorem Erdos1109.erdos_1109.variants.konyagin_upper Konyagin [Ko04] improved the upper bound to $f(N) \ll N^{11/15+o(1)}$ sorry line 103 source
Source documentation
Konyagin [Ko04] improved the upper bound to $f(N) \ll N^{11/15+o(1)}$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, Erdos1109.f, HPow.hPow, HAdd.hAdd, HDiv.hDiv
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_1109.variants.konyagin_upper :
    ∀ ε > (0 : ℝ), (fun N : ℕ => (f N : ℝ)) ≪
      fun N : ℕ => (N : ℝ) ^ ((11 : ℝ) / 15 + ε) := by
…
```
Mentions: Erdos1109.f