1. FormalConjectures
  2. ErdosProblems
  3. «423»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesUtil

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

@[expose] public sectionopen Finset BigOperators Filter Asymptoticsnamespace Erdos423

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)$.

def IsConsecutiveBlockSum (a : ℕ → ℕ) (k : ℕ) (m : ℕ) : Prop := ∃ i j : ℕ, 1 ≤ i ∧ i + 1 ≤ j ∧ j + 1 ≤ k ∧ m = ∑ l ∈ Finset.Icc i j, a l

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

def IsHofstadterSeq (a : ℕ → ℕ) : Prop := a 1 = 1 ∧ a 2 = 2 ∧ ∀ k : ℕ, 3 ≤ k → IsConsecutiveBlockSum a k (a k) ∧ a (k - 1) < a k ∧ ∀ m : ℕ, a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k m

The third term of the Hofstadter sequence is $a(3) = 3 = a(1) + a(2) = 1 + 2$.

a:ℕ → ℕha1:a 1 = 1ha2:a 2 = 2hk:∀ (k : ℕ), 3 ≤ k → IsConsecutiveBlockSum a k (a k) ∧ a (k - 1) < a k ∧ ∀ (m : ℕ), a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k mi:ℕj:ℕhi:1 ≤ ihij:i + 1 ≤ jhjk:j + 1 ≤ 3hsum:a 3 = ∑ l ∈ Icc i j, a lleft✝:a (3 - 1) < a 3right✝:∀ (m : ℕ), a (3 - 1) < m → m < a 3 → ¬IsConsecutiveBlockSum a 3 mthis:i = 1 ∧ j = 2⊢ a 3 = 3 a:ℕ → ℕha1:a 1 = 1ha2:a 2 = 2hk:∀ (k : ℕ), 3 ≤ k → IsConsecutiveBlockSum a k (a k) ∧ a (k - 1) < a k ∧ ∀ (m : ℕ), a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k mleft✝:a (3 - 1) < a 3right✝:∀ (m : ℕ), a (3 - 1) < m → m < a 3 → ¬IsConsecutiveBlockSum a 3 mhi:1 ≤ 1hjk:2 + 1 ≤ 3hij:1 + 1 ≤ 2hsum:a 3 = ∑ l ∈ Icc 1 2, a l⊢ a 3 = 3 a:ℕ → ℕha1:a 1 = 1ha2:a 2 = 2hk:∀ (k : ℕ), 3 ≤ k → IsConsecutiveBlockSum a k (a k) ∧ a (k - 1) < a k ∧ ∀ (m : ℕ), a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k mleft✝:a (3 - 1) < a 3right✝:∀ (m : ℕ), a (3 - 1) < m → m < a 3 → ¬IsConsecutiveBlockSum a 3 mhi:1 ≤ 1hjk:2 + 1 ≤ 3hij:1 + 1 ≤ 2hsum:a 3 = 1 + 2⊢ a 3 = 3 All goals completed! 🐙

The fourth term of the Hofstadter sequence is $a(4) = 5 = a(2) + a(3) = 2 + 3$.

All goals completed! 🐙

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)$.

@[category research open, AMS 5 11] theorem erdos_423 : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsHofstadterSeq a → (fun n : ℕ => (a n : ℝ) - n) =o[atTop] (fun n : ℕ => (n : ℝ)) := ⊢ True ↔ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → (fun n ↦ ↑(a n) - ↑n) =o[atTop] fun n ↦ ↑n All goals completed! 🐙

Bolan and Tang [Ta26] independently proved that $a_n-n$ is nondecreasing.

@[category research solved, AMS 5 11] theorem erdos_423.variants.nondecreasing : ∀ a : ℕ → ℕ, IsHofstadterSeq a → ∀ n m : ℕ, 1 ≤ n → n ≤ m → a n - n ≤ a m - m := ⊢ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → ∀ (n m : ℕ), 1 ≤ n → n ≤ m → a n - n ≤ a m - m All goals completed! 🐙

Bolan and Tang [Ta26] independently proved that $a_n-n\to\infty$.

@[category research solved, AMS 5 11] theorem erdos_423.variants.unbounded : ∀ a : ℕ → ℕ, IsHofstadterSeq a → ∀ M : ℕ, ∀ᶠ n in atTop, M + n ≤ a n := ⊢ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → ∀ (M : ℕ), ∀ᶠ (n : ℕ) in atTop, M + n ≤ a n All goals completed! 🐙

Bolan and Tang [Ta26] independently proved that infinitely many positive integers do not occur in the Hofstadter sequence.

@[category research solved, AMS 5 11] theorem erdos_423.variants.infinite_complement : ∀ a : ℕ → ℕ, IsHofstadterSeq a → Set.Infinite (Set.range a)ᶜ := ⊢ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → (Set.range a)ᶜ.Infinite All goals completed! 🐙

A Hofstadter sequence is strictly increasing from index 1 on.

a:ℕ → ℕh1:a 1 = 1h2:a 2 = 2hk:∀ (k : ℕ), 3 ≤ k → IsConsecutiveBlockSum a k (a k) ∧ a (k - 1) < a k ∧ ∀ (m : ℕ), a (k - 1) < m → m < a k → ¬IsConsecutiveBlockSum a k mk:ℕhpos:k > 0this:a (k + 2 - 1) < a (k + 2)⊢ a (k + 1) < a (k + 1 + 1) All goals completed! 🐙

A Hofstadter sequence satisfies n ≤ a n for n ≥ 1.

@[category API, AMS 5 11] theorem IsHofstadterSeq.le_apply {a : ℕ → ℕ} (ha : IsHofstadterSeq a) (n : ℕ) (hn : 1 ≤ n) : n ≤ a n := a:ℕ → ℕha:IsHofstadterSeq an:ℕhn:1 ≤ n⊢ n ≤ a n a:ℕ → ℕha:IsHofstadterSeq an:ℕhn:1 ≤ nh1:a 1 = 1⊢ n ≤ a n induction n, hn using Nat.le_induction with a:ℕ → ℕha:IsHofstadterSeq an:ℕh1:a 1 = 1⊢ 1 ≤ a 1 All goals completed! 🐙 a:ℕ → ℕha:IsHofstadterSeq an:ℕh1:a 1 = 1k:ℕhk:1 ≤ kih:k ≤ a k⊢ k + 1 ≤ a (k + 1) a:ℕ → ℕha:IsHofstadterSeq an:ℕh1:a 1 = 1k:ℕhk:1 ≤ kih:k ≤ a kthis:(fun k ↦ a (k + 1)) (k - 1) < (fun k ↦ a (k + 1)) (k - 1).succ⊢ k + 1 ≤ a (k + 1) a:ℕ → ℕha:IsHofstadterSeq an:ℕh1:a 1 = 1k:ℕhk:1 ≤ kih:k ≤ a kthis:a k < a (k + 1)⊢ k + 1 ≤ a (k + 1) All goals completed! 🐙

For indices ≥ 1, a Hofstadter sequence preserves and reflects <.

a:ℕ → ℕha:IsHofstadterSeq ai:ℕhi:1 ≤ i + 1j:ℕhj:1 ≤ j + 1⊢ i < j ↔ i + 1 < j + 1 All goals completed! 🐙

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.

a:ℕ → ℕha:IsHofstadterSeq ah:∀ (M : ℕ), ∀ᶠ (n : ℕ) in atTop, M + n ≤ a nN:ℕn✝:ℕhn✝:∀ (b : ℕ), n ≤ b → N + 2 + b ≤ a bn:ℕhn1:1 ≤ nhn:N + 2 + n ≤ a nhcard:#(image a (range n)) < #(Icc (N + 1) (a n - 1))k:ℕhx:N + 1 ≤ a k ∧ a k ≤ a n - 1hxi:a k ∉ image a (range n)hk:k ≥ nthis:a n ≤ a k⊢ False All goals completed! 🐙

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

a:ℕ → ℕha:IsHofstadterSeq ah:(Set.range a)ᶜ.InfiniteM:ℕt:Finset ℕhts:↑t ⊆ (Set.range a)ᶜhtc:#t = M + 1X:ℕ := t.sup idhX:X = t.sup idn:ℕhn:X + 1 ≤ nhn1:1 ≤ nA:Finset ℕ := image a (Icc 1 n)hA:A = image a (Icc 1 n)T:Finset ℕ := {x ∈ t | 1 ≤ x}hT:T = {x ∈ t | 1 ≤ x}hAcard:#A = nhTcard:M ≤ #Thdisj:Disjoint A Thsub:A ∪ T ⊆ Icc 1 (a n)this:n + #T ≤ a n + 1 - 1⊢ M + n ≤ a n All goals completed! 🐙

The unboundedness of $a_n-n$ is equivalent to the sequence omitting infinitely many positive integers.

@[category test, AMS 5 11] theorem erdos_423.test.unbounded_iff_infinite_complement : type_of% erdos_423.variants.unbounded ↔ type_of% erdos_423.variants.infinite_complement := ⟨fun h a ha => ha.infinite_compl_of_unbounded (h a ha), fun h a ha => ha.unbounded_of_infinite_compl (h a ha)⟩

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)}$.

@[category research solved, AMS 5 11] theorem erdos_423.variants.upper_bound : ∀ a : ℕ → ℕ, IsHofstadterSeq a → ∀ ε > (0 : ℝ), (fun n => (a n : ℝ)) =O[atTop] (fun n => (n : ℝ) ^ ((688 : ℝ) / 413 + ε)) := ⊢ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → ∀ ε > 0, (fun n ↦ ↑(a n)) =O[atTop] fun n ↦ ↑n ^ (688 / 413 + ε) All goals completed! 🐙

Tang [Ta26] proved the lower bound $a_n=n+\Omega(\log\log n)$.

@[category research solved, AMS 5 11] theorem erdos_423.variants.lower_bound : ∀ a : ℕ → ℕ, IsHofstadterSeq a → (fun n : ℕ => Real.log (Real.log n)) =O[atTop] (fun n : ℕ => (a n : ℝ) - n) := ⊢ ∀ (a : ℕ → ℕ), IsHofstadterSeq a → (fun n ↦ Real.log (Real.log ↑n)) =O[atTop] fun n ↦ ↑(a n) - ↑n All goals completed! 🐙end Erdos423