USA TSTST 2024 Problem 5

For a positive integer $k$, let $s(k)$ denote the number of $1$s in the binary representation of $k$. Prove that for any positive integer $n$,
$$\sum_{i=1}^{n}(-1)^{s(3i)} > 0.$$

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Nat.BitIndices
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Nat

theorem solution (n : ℕ) (hn : n > 0) :
    ∑ i ∈ (Finset.Icc 1 n), (-1) ^ (Nat.bitIndices (3 * i)).length > 0 := sorry

Login to submit a solution.