beaver_math_olympiad_problem_3

[BMO#3][https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#3._1RB0RB3LA4LA2RA_2LB3RA---3RA4RB_(bbch)_and_1RB1RB3LA4LA2RA_2LB3RA---3RA4RB_(bbch)] Let $v_2(n)$ be the largest integer $k$ such that $2^k$ divides $n$. Let $(a_n)_{n \ge 0}$ be a sequence such that $$a_n = \begin{cases} 2 & \text{if } n=0 \\ a_{n-1}+2^{v_2(a_{n-1})+2}-1 & \text{if } n \ge 1 \end{cases}$$ for all non-negative integers $n$. Is there an integer $n$ such that $a_n=4^k$ for some positive integer $k$? [BMO#3][https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#3._1RB0RB3LA4LA2RA_2LB3RA---3RA4RB_(bbch)_and_1RB1RB3LA4LA2RA_2LB3RA---3RA4RB_(bbch)] is equivalent to the non-termination of 2-state 5-symbol Turing machine [`1RB0RB3LA4LA2RA_2LB3RA---3RA4RB`](https://wiki.bbchallenge.org/wiki/1RB0RB3LA4LA2RA_2LB3RA---3RA4RB) (from all-0 tape). The machine was found and informally proven not to halt by [bbchallenge.org](bbchallenge.org) contributor Daniel Yuan on June 18th 2024; see [Discord discussion](https://discord.com/channels/960643023006490684/1084047886494470185/1252634913220591728).

theorem beaver_math_olympiad_problem_3
    (a : ℕ → ℕ)
    (a_ini : a 0 = 2)
    (a_rec : ∀ n, a (n + 1) = (a n) + 2 ^ ((padicValNat 2 (a n)) + 2) - 1) :
    ¬ (∃ n k, a n = 4 ^ k)

Recent Submissions

No submissions yet. Be the first to attempt this problem.