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

21 declarations, 17 contain sorry, 0 declared as axioms

Erdős Problem 357

References:

erdosproblems.com/357
[He86] Hegyvári, Norbert, On consecutive sums in sequences. Acta Math. Hungar. (1986), 193--200.

Imports (1)

FormalConjecturesUtil

def Erdos357.HasDistinctSums line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, AddCommMonoid
Proof uses: Set.InjOn, Finset, Finset.sum, Set.ofPred, Set.OrdConnected
2 instances, coercions and auxiliary constants left out.
def Erdos357.f Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct line 39 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Fin, Int, And, LE.le, Set, Set.range, Set.Icc, OfNat.ofNat, StrictMono, Erdos357.HasDistinctSums
13 instances, coercions and auxiliary constants left out.
```
noncomputable def f (n : ℕ) : ℕ :=
…
```
theorem Erdos357.erdos_357.parts.i Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 45 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Is $f(n)=o(n)$?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos357.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_357.parts.i : (fun n ↦ (f n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ)) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.parts.ii.bigO_version Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 63 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $g = O(f)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, sorryAx, Bool.false, Erdos357.f
Proof uses: Lean.Name, 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_357.parts.ii.bigO_version :
    (answer(sorry) : ℕ → ℝ) =O[atTop] (fun n ↦ (f n : ℝ)) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.parts.ii.bigO_version_symm Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 71 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = O(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos357.f, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.parts.ii.bigO_version_symm :
    (fun n ↦ (f n : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.parts.ii.bigTheta_version Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 79 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = \Theta(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos357.f, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.parts.ii.bigTheta_version :
    (fun n ↦ (f n : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.parts.ii.littleO_version Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 87 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $g = o(f)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, sorryAx, Bool.false, Erdos357.f
Proof uses: Lean.Name, 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_357.parts.ii.littleO_version :
    (answer(sorry) : ℕ → ℝ) =o[atTop] (fun n ↦ (f n : ℝ)) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.parts.ii.littleO_version_symm Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 95 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $f(n)$ grow? Can we find a (good) explicit function $g$ such that $f = o(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos357.f, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.parts.ii.littleO_version_symm :
    (fun n ↦ (f n : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.variants.weisenberg Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 105 source
Source documentation
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. It is known that $f(n) \geq (2+o(1))\sqrt{n}$. Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, Real.sqrt, Erdos357.f
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_357.variants.weisenberg : ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
    ∀ᶠ n in atTop, (2 + o n) * √n ≤ f n := by
…
```
Mentions: Erdos357.f
theorem Erdos357.erdos_357.variants.infinite_set_lower_density Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct sorry line 112 source
Source documentation
Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then $A$ has lower density 0.

depends on sorry what this means
Statement uses: Nat, StrictMono, Erdos357.HasDistinctSums, Eq, Real, Set.lowerDensity, Set.range, Set.univ, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_357.variants.infinite_set_lower_density (A : ℕ → ℕ) (hA : StrictMono A)
    (hA : HasDistinctSums A) : (Set.range A).lowerDensity = 0 := by
…
```
Mentions: Erdos357.HasDistinctSums
theorem Erdos357.erdos_357.variants.infinite_set_density Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct sorry line 119 source
Source documentation
Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then it is conjectured that $A$ has density 0.

depends on sorry what this means
Statement uses: Nat, StrictMono, Erdos357.HasDistinctSums, Set.HasDensity, Set.range, OfNat.ofNat, Real, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_357.variants.infinite_set_density (A : ℕ → ℕ) (hA : StrictMono A)
    (hA : HasDistinctSums A) :
    (Set.range A).HasDensity 0 := by
…
```
Mentions: Erdos357.HasDistinctSums
theorem Erdos357.erdos_357.variants.infinite_set_sum Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct sorry line 128 source
Source documentation
Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then it is conjectured that the sum $\sum_k \frac{1}{a_k}$ converges.

depends on sorry what this means
Statement uses: Nat, StrictMono, Erdos357.HasDistinctSums, Summable, Real, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_357.variants.infinite_set_sum (A : ℕ → ℕ) (hA : StrictMono A)
    (hA : HasDistinctSums A) :
    Summable (fun i ↦ (1 : ℝ) / A i) := by
…
```
Mentions: Erdos357.HasDistinctSums
def Erdos357.g Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct line 135 source
Source documentation
Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Fin, And, LE.le, Set, Set.range, Set.Icc, OfNat.ofNat, Erdos357.HasDistinctSums
7 instances, coercions and auxiliary constants left out.
```
noncomputable def g (n : ℕ) : ℕ :=
…
```
theorem Erdos357.erdos_357.variants.hegyvari Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 143 source
Source documentation
Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Hegyvári [He86] proved that $$\left(\frac 1 3 + o(1) \right)n \leq g(n) \leq \left(\frac 2 3 + o(1) \right)n.$$

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, Membership.mem, Set, Set.Icc, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Erdos357.g
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_357.variants.hegyvari : ∃ (o o' : ℕ → ℝ), o =o[atTop] (1 : ℕ → ℝ) ∧
    o' =o[atTop] (1 : ℕ → ℝ) ∧
      ∀ᶠ n in atTop, (g n : ℝ) ∈ Set.Icc ((1 / 3 + o n) * n) ((2 / 3 + o' n)*n) := by
…
```
Mentions: Erdos357.g
def Erdos357.h Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct line 150 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Fin, Int, And, LE.le, Set, Set.range, Set.Icc, OfNat.ofNat, Monotone, Erdos357.HasDistinctSums
13 instances, coercions and auxiliary constants left out.
```
noncomputable def h (n : ℕ) : ℕ :=
…
```
theorem Erdos357.erdos_357.variants.monotone.parts.i Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 160 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Is $h(n)=o(n)$?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos357.h
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_357.variants.monotone.parts.i : (fun n ↦ (h n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ)) := by
…
```
Mentions: Erdos357.h
theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 167 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $g = O(h)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, sorryAx, Bool.false, Erdos357.h
Proof uses: Lean.Name, 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_357.variants.monotone.parts.ii.bigO_version :
    (answer(sorry) : ℕ → ℝ) =O[atTop] (fun n ↦ (h n : ℝ)) := by
…
```
Mentions: Erdos357.h
theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version_symm Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 175 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = O(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos357.h, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.variants.monotone.parts.ii.bigO_version_symm :
    (fun n ↦ (h n : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.h
theorem Erdos357.erdos_357.variants.monotone.parts.ii.bigTheta_version Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 183 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = \Theta(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos357.h, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.variants.monotone.parts.ii.bigTheta_version :
    (fun n ↦ (h n : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.h
theorem Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 191 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $g = o(h)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, sorryAx, Bool.false, Erdos357.h
Proof uses: Lean.Name, 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_357.variants.monotone.parts.ii.littleO_version :
    (answer(sorry) : ℕ → ℝ) =o[atTop] (fun n ↦ (h n : ℝ)) := by
…
```
Mentions: Erdos357.h
theorem Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version_symm Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct sorry line 199 source
Source documentation
Let $h(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 \leq \dotsc \leq a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. How does $h(n)$ grow? Can we find a (good) explicit function $g$ such that $h = o(g)$ ?

depends on sorry what this means
Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos357.h, sorryAx, Bool.false
Proof uses: Lean.Name, 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_357.variants.monotone.parts.ii.littleO_version_symm :
    (fun n ↦ (h n : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos357.h