A sequence that looks back half way
If a(n) drops by a(⌊n/2⌋)/n at each odd step, then n a(n) tends to 1/(1 − ln 2), as a commenter guessed from the digits.
Open problem settled, formally verified in Lean 4
Let a(1) = 1, a(n) = a(n−1) for even n, and a(n) = a(n−1) − a((n−1)/2)/n for odd n. The user AAK asked on Mathematics Stack Exchange (question 4748129) for the constant A with n a(n) → A; Tian Vlasic suggested A = 1/(1 − ln 2) from its digits. This note proves it (Theorem 1).
The key is an exact identity (Lemma 2): n a(n) = 1 + Σ a(k) over the window n/2 ≤ k < n. It makes n a(n) equal to 1 plus a weighted average of earlier values, with total weight tending to ln 2 < 1 (Lemma 3, from Euler’s constant). The error e(n) = n a(n) − A then satisfies |e(n)| ≤ s(n) max |e(k)| + A |s(n) − ln 2| over the window, and since s(n) ≤ 3/4 eventually, the error shrinks to zero.
Preprint v1, 10 October 2026, not peer reviewed. Every step of the proof is formally verified in Lean 4 (lean/, standard axioms only); the rate in Remark 4 is numerical. An answer with this proof was posted to the question (answer 5150836). The author used AI tools (Claude, Anthropic) in this work, as described in the paper’s acknowledgement, and is responsible for its content.