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

5 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 796

Reference: erdosproblems.com/796

Imports (1)

FormalConjecturesUtil

def Erdos796.repCount The number of unordered representations m = a₁ * a₂ by two distinct elements a₁ < a₂ of A line 35 source
Source documentation
The number of unordered representations m = a₁ * a₂ by two distinct elements a₁ < a₂ of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Finset.card, Prod, Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Eq, HMul.hMul, SProd.sprod
7 instances, coercions and auxiliary constants left out.
```
def repCount (A : Finset ℕ) (m : ℕ) : ℕ :=
…
```
def Erdos796.HasRepBound A has at most k - 1 representations of every m (fewer than k) line 39 source
Source documentation
A has at most k - 1 representations of every m (fewer than k).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: LT.lt, Erdos796.repCount
1 instances, coercions and auxiliary constants left out.
```
def HasRepBound (k : ℕ) (A : Finset ℕ) : Prop := ∀ m : ℕ, repCount A m < k
…
```
Mentions: Erdos796.repCount
def Erdos796.g g k n = g_k(n) is the largest size of a subset A ⊆ {1, …, n} in which every m has fewer than k representations m = a₁ a₂ with a₁ < a₂ ∈ A line 44 source
Source documentation
g k n = g_k(n) is the largest size of a subset A ⊆ {1, …, n} in which every m has fewer than k representations m = a₁ a₂ with a₁ < a₂ ∈ A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sup, Finset, Finset.filter, Erdos796.HasRepBound, Classical.propDecidable, Finset.powerset, Finset.Icc, OfNat.ofNat, Finset.card
6 instances, coercions and auxiliary constants left out.
```
noncomputable def g (k n : ℕ) : ℕ :=
…
```
def Erdos796.normalizedError The proposed second-order rescaling of g_3(n): (g_3(n) - (log log n / log n) · n) / (n / log n), whose limit is the constant c in the problem line 50 source
Source documentation
The proposed second-order rescaling of g_3(n): (g_3(n) - (log log n / log n) · n) / (n / log n), whose limit is the constant c in the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, HSub.hSub, Erdos796.g, OfNat.ofNat, HMul.hMul, Real.log
10 instances, coercions and auxiliary constants left out.
```
noncomputable def normalizedError (n : ℕ) : ℝ :=
…
```
theorem Erdos796.erdos_796 Let $k\geq 2$ and let $g_k(n)$ be the largest possible size of $A\subseteq \{1,\ldots,n\}$ such that every $m$ has $<k$ solutions to $m=a_1a_2$ with $a_1<a_2\in A$ sorry line 63 source
Source documentation
Let $k\geq 2$ and let $g_k(n)$ be the largest possible size of $A\subseteq \{1,\ldots,n\}$ such that every $m$ has $<k$ solutions to $m=a_1a_2$ with $a_1<a_2\in A$. Is it true that $$g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}$$ for some constant $c$?
The answer is yes: the rescaled error normalizedError converges.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, Filter.Tendsto, Nat, Erdos796.normalizedError, Filter.atTop, nhds
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_796 :
    answer(True) ↔ ∃ c : ℝ, Tendsto normalizedError atTop (𝓝 c) := by
…
```
Mentions: c, Erdos796.normalizedError