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

16 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 423

References:

erdosproblems.com/423
[Er77c] Erdős, P., Problems and results on combinatorial number theory. III, Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique (1980).
[Cu25] Cushman, A., A Note on the Sum-Product Problem and the Convex Sumset Problem. arXiv:2512.13849 (2025).
[Ta26] Tang, Q., The Hofstadter consecutive-sum sequence omits infinitely many positive integers. arXiv:2603.09939 (2026).
[Bolan] Bolan, M., Hofstader–Ulam Sequence, https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf
OEIS A005243

Imports (1)

FormalConjecturesUtil

def Erdos423.IsConsecutiveBlockSum IsConsecutiveBlockSum a k m means that $m$ equals the sum of at least two consecutive terms of the sequence $a$, using indices from $\{1, \ldots, k - 1\}$ line 48 source
Source documentation
IsConsecutiveBlockSum a k m means that $m$ equals the sum of at least two consecutive terms of the sequence $a$, using indices from $\{1, \ldots, k - 1\}$. That is, there exist $i, j$ with $1 \le i$, $i + 1 \le j$, $j \le k - 1$ such that $m = a(i) + a(i+1) + \cdots + a(j)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, And, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Finset.sum, Finset.Icc
7 instances, coercions and auxiliary constants left out.
```
def IsConsecutiveBlockSum (a : ℕ → ℕ) (k : ℕ) (m : ℕ) : Prop :=
…
```
def Erdos423.IsHofstadterSeq The Hofstadter sequence (OEIS A005243) line 55 source
Source documentation
The Hofstadter sequence (OEIS A005243): $a(1) = 1$, $a(2) = 2$, and for $k \ge 3$, $a(k)$ is the least integer $> a(k-1)$ that equals the sum of at least two consecutive terms from $\{a(1), \ldots, a(k-1)\}$. The sequence begins $1, 2, 3, 5, 6, 8, 10, 11, \ldots$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, Eq, OfNat.ofNat, LE.le, Erdos423.IsConsecutiveBlockSum, LT.lt, HSub.hSub, Not
5 instances, coercions and auxiliary constants left out.
```
def IsHofstadterSeq (a : ℕ → ℕ) : Prop :=
…
```
theorem Erdos423.erdos_423.test.a3 The third term of the Hofstadter sequence is $a(3) = 3 = a(1) + a(2) = 1 + 2$ line 64 source
Source documentation
The third term of the Hofstadter sequence is $a(3) = 3 = a(1) + a(2) = 1 + 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Eq, OfNat.ofNat
Proof uses: LE.le, And, Erdos423.IsConsecutiveBlockSum, LT.lt, HSub.hSub, Not, Decidable.byContradiction, Exists, HAdd.hAdd, Finset.sum, Finset.Icc, Eq.mp, congrArg, Eq.trans, Insert.insert, Finset, Singleton.singleton, Finset.sum_congr, of_decide_eq_true, id and 10 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423.test.a3 : ∀ a : ℕ → ℕ, IsHofstadterSeq a → a 3 = 3 := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.test.a4 The fourth term of the Hofstadter sequence is $a(4) = 5 = a(2) + a(3) = 2 + 3$ line 75 source
Source documentation
The fourth term of the Hofstadter sequence is $a(4) = 5 = a(2) + a(3) = 2 + 3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Eq, OfNat.ofNat
Proof uses: LE.le, And, Erdos423.IsConsecutiveBlockSum, LT.lt, HSub.hSub, Not, Erdos423.erdos_423.test.a3, And.intro, Decidable.byContradiction, Exists, HAdd.hAdd, Finset.sum, Finset.Icc, Or, Eq.mp, congrArg, Eq.trans, Insert.insert, Finset, Singleton.singleton and 17 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423.test.a4 : ∀ a : ℕ → ℕ, IsHofstadterSeq a → a 4 = 5 := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423 Documented declaration: erdos_423 sorry line 110 source
Source documentation
Erdős Problem 423 [Er77c, p.71; ErGr80, p.83]:
Let $a(1) = 1$, $a(2) = 2$, and for $k \ge 3$ let $a(k)$ be the least integer greater than $a(k-1)$ that is a sum of at least two consecutive terms of the sequence. What is the asymptotic behaviour of this sequence? It seems likely that $a_n = n + o(n)$.

depends on sorry what this means
Statement uses: Iff, True, Nat, Erdos423.IsHofstadterSeq, Asymptotics.IsLittleO, Real, Filter.atTop, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423 : answer(sorry) ↔
    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
    (fun n : ℕ => (a n : ℝ) - n) =o[atTop] (fun n : ℕ => (n : ℝ)) := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.variants.nondecreasing Bolan and Tang [Ta26] independently proved that $a_n-n$ is nondecreasing sorry line 119 source
Source documentation
Bolan and Tang [Ta26] independently proved that $a_n-n$ is nondecreasing.

depends on sorry what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, LE.le, OfNat.ofNat, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423.variants.nondecreasing :
    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
    ∀ n m : ℕ, 1 ≤ n → n ≤ m → a n - n ≤ a m - m := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.variants.unbounded Bolan and Tang [Ta26] independently proved that $a_n-n\to\infty$ sorry line 128 source
Source documentation
Bolan and Tang [Ta26] independently proved that $a_n-n\to\infty$.

depends on sorry what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Filter.Eventually, LE.le, HAdd.hAdd, Filter.atTop
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_423.variants.unbounded :
    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
    ∀ M : ℕ, ∀ᶠ n in atTop, M + n ≤ a n := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.variants.infinite_complement Bolan and Tang [Ta26] independently proved that infinitely many positive integers do not occur in the Hofstadter sequence sorry line 138 source
Source documentation
Bolan and Tang [Ta26] independently proved that infinitely many positive integers do not occur in the Hofstadter sequence.

depends on sorry what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Set.Infinite, Compl.compl, Set, Set.range
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423.variants.infinite_complement :
    ∀ a : ℕ → ℕ, IsHofstadterSeq a → Set.Infinite (Set.range a)ᶜ := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.IsHofstadterSeq.strictMono A Hofstadter sequence is strictly increasing from index 1 on line 144 source
Source documentation
A Hofstadter sequence is strictly increasing from index 1 on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, StrictMono, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, And, LE.le, Erdos423.IsConsecutiveBlockSum, LT.lt, HSub.hSub, Not, strictMono_nat_of_lt_succ, id, GT.gt, Or, Nat.eq_zero_or_pos, Decidable.byContradiction, Eq.symm, And.left, And.right, Eq.mpr
21 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem IsHofstadterSeq.strictMono {a : ℕ → ℕ} (ha : IsHofstadterSeq a) :
    StrictMono fun k => a (k + 1) := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.IsHofstadterSeq.le_apply A Hofstadter sequence satisfies n ≤ a n for n ≥ 1 line 157 source
Source documentation
A Hofstadter sequence satisfies n ≤ a n for n ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, LE.le, OfNat.ofNat
Proof uses: Eq, And.left, And, Erdos423.IsConsecutiveBlockSum, LT.lt, HSub.hSub, Not, Nat.le_induction, Decidable.byContradiction, HAdd.hAdd, Nat.succ, Erdos423.IsHofstadterSeq.strictMono, Nat.lt_succ_self, Eq.mp, congr, congrArg
17 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem IsHofstadterSeq.le_apply {a : ℕ → ℕ} (ha : IsHofstadterSeq a) (n : ℕ)
    (hn : 1 ≤ n) : n ≤ a n := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.IsHofstadterSeq.lt_iff_lt For indices ≥ 1, a Hofstadter sequence preserves and reflects < line 169 source
Source documentation
For indices ≥ 1, a Hofstadter sequence preserves and reflects <.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, LE.le, OfNat.ofNat, Iff, LT.lt
Proof uses: Eq, HAdd.hAdd, Exists, Nat.exists_eq_add_of_le', Eq.mpr, id, congrArg, propext, StrictMono.lt_iff_lt, Erdos423.IsHofstadterSeq.strictMono, Decidable.byContradiction, Not, Eq.symm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem IsHofstadterSeq.lt_iff_lt {a : ℕ → ℕ} (ha : IsHofstadterSeq a) {i j : ℕ}
    (hi : 1 ≤ i) (hj : 1 ≤ j) :
    a i < a j ↔ i < j := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.IsHofstadterSeq.infinite_compl_of_unbounded Documented declaration: infinite_compl_of_unbounded line 181 source
Source documentation
If a n - n is unbounded, infinitely many integers are missed: when a n ≥ N + 2 + n, the n values a 0, …, a (n - 1) cannot cover the n + 1 integers in [N + 1, a n - 1], and later terms are too large.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Filter.Eventually, LE.le, HAdd.hAdd, Filter.atTop, Set.Infinite, Compl.compl, Set, Set.range
Proof uses: Set.infinite_of_forall_exists_gt, OfNat.ofNat, Exists, And, Membership.mem, LT.lt, Filter.Eventually.exists_forall_of_atTop, Exists.intro, Max.max, And.intro, Decidable.byContradiction, Not, le_max_left, Finset.card, Finset.image, Finset.range, Finset.Icc, HSub.hSub, Trans.trans, Eq.mp and 29 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem IsHofstadterSeq.infinite_compl_of_unbounded {a : ℕ → ℕ} (ha : IsHofstadterSeq a)
    (h : ∀ M : ℕ, ∀ᶠ n in atTop, M + n ≤ a n) : Set.Infinite (Set.range a)ᶜ := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.IsHofstadterSeq.unbounded_of_infinite_compl If infinitely many integers are missed, a n - n is unbounded: M + 1 missed integers below n together with a 1, …, a n are distinct elements of [1, a n] line 207 source
Source documentation
If infinitely many integers are missed, a n - n is unbounded: M + 1 missed integers below n together with a 1, …, a n are distinct elements of [1, a n].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Set.Infinite, Compl.compl, Set, Set.range, Filter.Eventually, LE.le, HAdd.hAdd, Filter.atTop
Proof uses: Finset, And, Eq, Finset.card, OfNat.ofNat, Exists, Set.Infinite.exists_subset_card_eq, Finset.sup, id, rfl, Eq.mpr, congrArg, propext, Filter.eventually_atTop, Exists.intro, Decidable.byContradiction, Not, Finset.image, Finset.Icc, Finset.filter and 40 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
```
theorem IsHofstadterSeq.unbounded_of_infinite_compl {a : ℕ → ℕ} (ha : IsHofstadterSeq a)
    (h : Set.Infinite (Set.range a)ᶜ) : ∀ M : ℕ, ∀ᶠ n in atTop, M + n ≤ a n := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.test.unbounded_iff_infinite_complement The unboundedness of $a_n-n$ is equivalent to the sequence omitting infinitely many positive integers line 263 source
Source documentation
The unboundedness of $a_n-n$ is equivalent to the sequence omitting infinitely many positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, Nat, Erdos423.IsHofstadterSeq, Filter.Eventually, LE.le, HAdd.hAdd, Filter.atTop, Set.Infinite, Compl.compl, Set, Set.range
Proof uses: Iff.intro, Erdos423.IsHofstadterSeq.infinite_compl_of_unbounded, Erdos423.IsHofstadterSeq.unbounded_of_infinite_compl
10 instances, coercions and auxiliary constants left out.
```
theorem erdos_423.test.unbounded_iff_infinite_complement :
    type_of% erdos_423.variants.unbounded ↔
      type_of% erdos_423.variants.infinite_complement :=
…
```
Mentions: Erdos423.erdos_423.variants.unbounded, Erdos423.erdos_423.variants.infinite_complement
theorem Erdos423.erdos_423.variants.upper_bound Tang [Ta26] proved $a_n \ll n^{1/(c-1)+o(1)}$ whenever every finite convex set $A$ satisfies $|A-A|\geq |A|^{c-o(1)}$ sorry line 275 source
Source documentation
Tang [Ta26] proved $a_n \ll n^{1/(c-1)+o(1)}$ whenever every finite convex set $A$ satisfies $|A-A|\geq |A|^{c-o(1)}$. Using the bound of Cushman [Cu25] gives $a_n\ll n^{688/413+o(1)}$.

depends on sorry what this means
Statement uses: Nat, Erdos423.IsHofstadterSeq, Real, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Filter.atTop, 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_423.variants.upper_bound :
    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
    ∀ ε > (0 : ℝ), (fun n => (a n : ℝ)) =O[atTop]
      (fun n => (n : ℝ) ^ ((688 : ℝ) / 413 + ε)) := by
…
```
Mentions: Erdos423.IsHofstadterSeq
theorem Erdos423.erdos_423.variants.lower_bound Tang [Ta26] proved the lower bound $a_n=n+\Omega(\log\log n)$ sorry line 285 source
Source documentation
Tang [Ta26] proved the lower bound $a_n=n+\Omega(\log\log n)$.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_423.variants.lower_bound :
    ∀ a : ℕ → ℕ, IsHofstadterSeq a →
    (fun n : ℕ => Real.log (Real.log n)) =O[atTop]
      (fun n : ℕ => (a n : ℝ) - n) := by
…
```
Mentions: Erdos423.IsHofstadterSeq