1. FormalConjectures
  2. ErdosProblems
  3. «346»
/- 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 346

References:

    erdosproblems.com/346

    [Gr64d] Graham, R. L., A property of Fibonacci numbers. Fibonacci Quart. (1964), 1-10.

    [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

@[expose] public sectionopen Filter Topology Setnamespace Erdos346

Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?

The answer is no. A counterexample recorded at [erdosproblems.com/346] has all successive ratios at least 6 / 5, but has subsequences of successive ratios tending to two different limits, (1 + √5) / 2 and (1 + √5) / 2 + 1 / 4.

@[category research solved, AMS 11] theorem erdos_346 : answer(False) ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) → Tendsto (fun n => A (n + 1) / (A n : ℝ)) atTop (𝓝 ((1 + √5) / 2)) := ⊢ False ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ B ⊆ range A, B.Infinite → ¬IsAddComplete (range A \ B)) → Tendsto (fun n ↦ ↑(A (n + 1)) / ↑(A n)) atTop (𝓝 ((1 + √5) / 2)) All goals completed! 🐙

We define a sequence f by the formula f n = n.fib - (- 1) ^ n.

def f (n : ℕ) : ℕ := if Even n then n.fib - 1 else n.fib + 1

The sequence f is lacunary.

k:ℕhk:9 ≤ khfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)hfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1))hpos:1 ≤ Nat.fib khpos1:1 ≤ Nat.fib (k + 1)heven:¬Even khodd_plus:Even (k + 1)⊢ 3 / 2 * ↑(Nat.fib k + 1) < ↑(Nat.fib (k + 1) - 1) k:ℕhk:9 ≤ khfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)hfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1))hpos:1 ≤ Nat.fib khpos1:1 ≤ Nat.fib (k + 1)heven:¬Even khodd_plus:Even (k + 1)⊢ 3 / 2 * (↑(Nat.fib k) + 1) < ↑(Nat.fib (k + 1)) - 1 All goals completed! 🐙

The sequence f is strongly complete, and this is proved in [Gr64d].

@[category research solved, AMS 11] theorem erdos_346.variants.f_isAddStronglyCompleteNatSeq : IsAddStronglyCompleteNatSeq f := ⊢ IsAddStronglyCompleteNatSeq f All goals completed! 🐙

The recurrence f (m + 2) = f (m + 1) + f m - (-1) ^ m for m ≥ 1, written without subtraction.

m:ℕhm:1 ≤ mh1:1 ≤ Nat.fib mh2:1 ≤ Nat.fib (m + 1)h3:Nat.fib (m + 2) = Nat.fib m + Nat.fib (m + 1)he:¬Even mhe1:Even (m + 1)he2:¬Even (m + 2)⊢ (f (m + 2) + if Even m then 1 else 0) = f (m + 1) + f m + if Even m then 0 else 1 m:ℕhm:1 ≤ mh1:1 ≤ Nat.fib mh2:1 ≤ Nat.fib (m + 1)h3:Nat.fib (m + 2) = Nat.fib m + Nat.fib (m + 1)he:¬Even mhe1:Even (m + 1)he2:¬Even (m + 2)⊢ Nat.fib (m + 2) + 1 + 0 = Nat.fib (m + 1) - 1 + (Nat.fib m + 1) + 1 All goals completed! 🐙

f 0 + ⋯ + f (m - 1) = f (m + 1) - [m even] for m ≥ 1; this is [Gr64d, Eq. (1)].

k:ℕih:1 ≤ k → (∑ i ∈ Finset.range k, f i + if Even k then 1 else 0) = f (k + 1)hm:1 ≤ k + 1hk:k > 0h1:(∑ i ∈ Finset.range k, f i + if Even k then 1 else 0) = f (k + 1)h2:(f (k + 1 + 1) + if Even k then 1 else 0) = f (k + 1) + f k + if Even k then 0 else 1hpar:((if Even (k + 1) then 1 else 0) + if Even k then 1 else 0) = 1hpar':((if Even k then 1 else 0) + if Even k then 0 else 1) = 1⊢ (∑ x ∈ Finset.range k, f x + f k + if Even (k + 1) then 1 else 0) = f (k + 1 + 1) All goals completed! 🐙

f is strictly increasing from index 4 on.

k:ℕh:(f (3 + k + 2) + if Even (3 + k) then 1 else 0) = f (3 + k + 1) + f (3 + k) + if Even (3 + k) then 0 else 1hf:2 ≤ f (3 + k)⊢ f (3 + k + 1) < f (3 + k + 2) k:ℕhf:2 ≤ f (3 + k)h✝:Even (3 + k)h:f (3 + k + 2) + 1 = f (3 + k + 1) + f (3 + k) + 0⊢ f (3 + k + 1) < f (3 + k + 2)k:ℕhf:2 ≤ f (3 + k)h✝:¬Even (3 + k)h:f (3 + k + 2) + 0 = f (3 + k + 1) + f (3 + k) + 1⊢ f (3 + k + 1) < f (3 + k + 2) k:ℕhf:2 ≤ f (3 + k)h✝:Even (3 + k)h:f (3 + k + 2) + 1 = f (3 + k + 1) + f (3 + k) + 0⊢ f (3 + k + 1) < f (3 + k + 2)k:ℕhf:2 ≤ f (3 + k)h✝:¬Even (3 + k)h:f (3 + k + 2) + 0 = f (3 + k + 1) + f (3 + k) + 1⊢ f (3 + k + 1) < f (3 + k + 2) All goals completed! 🐙

The sequence f is not complete whenever infinitely many terms are removed from it, and this is proved in [Gr64d].

B:Set ℕh:B ⊆ range fhB:B.Infinitem:ℕhm:4 ≤ mthis:(∑ i ∈ Finset.range m, f i + if Even m then 1 else 0) = f (m + 1)⊢ ∑ i ∈ Finset.range m, f i ≤ f (m + 1); All goals completed! 🐙) h hB

Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.

@[category research solved, AMS 11] theorem erdos_346.variants.gt_goldenRatio_not_IsAddComplete {A : ℕ → ℕ} (hA : ∀ n, (1 + √5) / 2 * A n < A (n + 1)) {B : Set ℕ} (h : B ⊆ range A) (hB : B.Infinite) : ¬ IsAddComplete (range A \ B) := A:ℕ → ℕhA:∀ (n : ℕ), (1 + √5) / 2 * ↑(A n) < ↑(A (n + 1))B:Set ℕh:B ⊆ range AhB:B.Infinite⊢ ¬IsAddComplete (range A \ B) All goals completed! 🐙

Erdős and Graham [ErGr80] also say that it is not hard to construct very irregular sequences satisfying the aforementioned properties: there is a strictly increasing sequence A that is strongly complete and not complete whenever infinitely many terms are removed from it, but with $\liminf_n A(n+1)/A(n) = 1$ and $\limsup_n A(n+1)/A(n) = \infty$.

@[category research solved, AMS 11] theorem erdos_346.variants.example : ∃ A : ℕ → ℕ, StrictMono A ∧ IsAddStronglyCompleteNatSeq A ∧ (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) ∧ liminf (fun n => A (n + 1) / (A n : ℝ)) atTop = 1 ∧ limsup (fun n => A (n + 1) / (A n : ENNReal)) atTop = ⊤ := ⊢ ∃ A, StrictMono A ∧ IsAddStronglyCompleteNatSeq A ∧ (∀ B ⊆ range A, B.Infinite → ¬IsAddComplete (range A \ B)) ∧ liminf (fun n ↦ ↑(A (n + 1)) / ↑(A n)) atTop = 1 ∧ limsup (fun n ↦ ↑(A (n + 1)) / ↑(A n)) atTop = ⊤ All goals completed! 🐙end Erdos346