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

8 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 1192

References:

erdosproblems.com/1192
[Ru90] Ruzsa, Imre Z., A just basis. Monatsh. Math. (1990), 145--151.
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89--115.

Imports (1)

FormalConjecturesUtil

def Erdos1192.f_r For $A\subset \mathbb{N}$ let $f_r(n)$ count the number of solutions to $n=a_1+\cdots+a_r$ with $a_i\in A$ line 41 source
Source documentation
For $A\subset \mathbb{N}$ let $f_r(n)$ count the number of solutions to $n=a_1+\cdots+a_r$ with $a_i\in A$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, Fin, Set.ofPred, And, Membership.mem, Eq, Finset.sum, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def f_r (A : Set ℕ) (r n : ℕ) : ℕ :=
…
```
theorem Erdos1192.erdos_1192.f_r_zero_zero The empty sum ($r = 0$) gives exactly one representation of $0$: the empty tuple line 46 source
Source documentation
The empty sum ($r = 0$) gives exactly one representation of $0$: the empty tuple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos1192.f_r, OfNat.ofNat
Proof uses: id, Fin, Set.ofPred, And, Membership.mem, Finset.sum, Finset.univ, Singleton.singleton, Inhabited.default, Set.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, Set.univ, congrFun', funext, Finset.sum_congr and 10 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.f_r_zero_zero (A : Set ℕ) : f_r A 0 0 = 1 := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192.f_r_empty With an empty set, there are no valid $r$-tuples for $r \geq 1$ line 55 source
Source documentation
With an empty set, there are no valid $r$-tuples for $r \geq 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos1192.f_r, EmptyCollection.emptyCollection, Set, HAdd.hAdd, OfNat.ofNat
Proof uses: id, Fin, Set.ofPred, And, Membership.mem, Finset.sum, Finset.univ, Set.ext, of_eq_true, Iff, Eq.trans, False, True, congr, congrArg, congrFun', funext, forall_congr, false_and, iff_self and 4 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.f_r_empty (r n : ℕ) : f_r ∅ (r + 1) n = 0 := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192.f_r_singleton_self For $r = 1$, $f_1(\{n\}, n) = 1$: the only $1$-tuple from $\{n\}$ summing to $n$ is $(n)$ line 64 source
Source documentation
For $r = 1$, $f_1(\{n\}, n) = 1$: the only $1$-tuple from $\{n\}$ summing to $n$ is $(n)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos1192.f_r, Singleton.singleton, Set, OfNat.ofNat
Proof uses: id, Fin, Set.ofPred, And, Membership.mem, Finset.sum, Finset.univ, Set.ext, Eq.mpr, Iff, congr, congrArg, congrFun', funext, forall_congr, Iff.intro, And.intro, rfl, of_eq_true, Eq.trans and 14 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.f_r_singleton_self (n : ℕ) : f_r {n} 1 n = 1 := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192.f_r_no_rep $f_1(\{0\}, 1) = 0$: can't represent $1$ with a single element from $\{0\}$ line 80 source
Source documentation
$f_1(\{0\}, 1) = 0$: can't represent $1$ with a single element from $\{0\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos1192.f_r, Singleton.singleton, Set, OfNat.ofNat
Proof uses: id, Fin, Set.ofPred, And, Membership.mem, Finset.sum, Finset.univ, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Not, Eq.trans, False, congr, congrArg, congrFun', funext, forall_congr, iff_false and 11 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.f_r_no_rep : f_r {0} 1 1 = 0 := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192 Does there exist, for all $r\geq 2$, a basis $A$ of order $r$ (so that $f_r(n)>0$ for all large $n$) such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ for all $x$? sorry line 97 source
Source documentation
Does there exist, for all $r\geq 2$, a basis $A$ of order $r$ (so that $f_r(n)>0$ for all large $n$) such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ for all $x$?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, Set, And, Filter.Eventually, GT.gt, Erdos1192.f_r, Filter.atTop, Asymptotics.IsBigO, Real, Finset.sum, Finset.range, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192 :
    answer(sorry) ↔
      ∀ r ≥ 2, ∃ A : Set ℕ,
        (∀ᶠ n in atTop, f_r A r n > 0) ∧
        (fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A r n : ℝ) ^ 2) =O[atTop]
          (fun (x : ℕ) ↦ (x : ℝ)) := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192.variants.renyi Erdős and Rényi proved by the probabilistic method that there exists a set $A$ such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ and $$\lvert A\cap [1,x]\rvert\gg x^{1/r}$$ for all $x$ sorry line 111 source
Source documentation
Erdős and Rényi proved by the probabilistic method that there exists a set $A$ such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ and $$\lvert A\cap [1,x]\rvert\gg x^{1/r}$$ for all $x$.

depends on sorry what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Exists, Set, And, Asymptotics.IsBigO, Real, Filter.atTop, Finset.sum, Finset.range, HAdd.hAdd, HPow.hPow, Erdos1192.f_r, HDiv.hDiv, Nat.count, Membership.mem, Classical.propDecidable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.variants.renyi :
    ∀ r ≥ 2, ∃ A : Set ℕ,
      ((fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A r n : ℝ) ^ 2) =O[atTop]
        (fun (x : ℕ) ↦ (x : ℝ))) ∧
      ((fun (x : ℕ) ↦ (x : ℝ) ^ (1 / (r : ℝ))) =O[atTop]
        (fun (x : ℕ) ↦ (count (· ∈ A) x : ℝ))) := by
…
```
Mentions: Erdos1192.f_r
theorem Erdos1192.erdos_1192.variants.ruzsa Ruzsa [Ru90] proved that the answer is yes for $r=2$ sorry line 123 source
Source documentation
Ruzsa [Ru90] proved that the answer is yes for $r=2$.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, Filter.Eventually, GT.gt, Erdos1192.f_r, OfNat.ofNat, Filter.atTop, Asymptotics.IsBigO, Real, Finset.sum, Finset.range, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1192.variants.ruzsa :
    ∃ A : Set ℕ,
      (∀ᶠ n in atTop, f_r A 2 n > 0) ∧
      (fun (x : ℕ) ↦ ∑ n ∈ range (x + 1), (f_r A 2 n : ℝ) ^ 2) =O[atTop]
        (fun (x : ℕ) ↦ (x : ℝ)) := by
…
```
Mentions: Erdos1192.f_r