module
public import Mathlib.Tactic
public import Mathlib.Data.Nat.Find
public import Mathlib.Logic.Relation
public import Mathlib.Algebra.Order.GroupWithZero.Basic
public section
/-!
# USA Mathematical Olympiad 2026, Problem 2
Annie is playing a game where she starts with a row of positive integers, written
on a blackboard, each of which is a power of 2. On each turn, she can erase two
adjacent numbers and replace them with a power of 2 that is greater than either of
the erased numbers. This shortens the row of numbers, and she continues to take
turns until only one number remains. Annie wins the game if the final remaining
number is less than 4 times the sum of the original numbers. Is it always possible
for Annie to win, regardless of the starting row of numbers?
-/
namespace Usa2026P2
/-- A positive integer which is a power of two (in particular `1 = 2 ^ 0` counts). -/
def IsPow2 (x : ℕ) : Prop := ∃ k, x = 2 ^ k
/-- One legal turn of the game: the two adjacent entries `x` and `y` are erased and
replaced by a power of two `z` which is strictly larger than both of them. -/
inductive Move : List ℕ → List ℕ → Prop
| mk (l r : List ℕ) (x y z : ℕ) (hz : IsPow2 z) (hx : x < z) (hy : y < z) :
Move (l ++ x :: y :: r) (l ++ z :: r)
/-- The answer is **yes**: from any starting row of powers of two, Annie can always
reach a single number which is less than four times the sum of the starting row. -/
theorem usa2026_p2 (a : List ℕ) (ha : a ≠ []) (hp : ∀ x ∈ a, IsPow2 x) :
∃ m, Relation.ReflTransGen Move a [m] ∧ m < 4 * a.sum := sorry
end Usa2026P2
This problem has a complete formalized solution.