Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2010P5

import Mathlib.Algebra.Group.Fin.Basic
import Mathlib.Algebra.Order.Pi
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Algebra.Order.Sub.Basic
import Mathlib.Algebra.Order.Sub.Prod
import Mathlib.Data.Fintype.Basic

/-!
# International Mathematical Olympiad 2010, Problem 5

Each of the six boxes $B_1, B_2, B_3, B_4, B_5, B_6$ initially contains one coin.
The following two types of operations are allowed:

1. Choose a non-empty box $B_j, 1 ≤ j ≤ 5$, remove one coin from $B_j$ and
add two coins to $B_{j+1}$;
2. Choose a non-empty box $B_k, 1 ≤ k ≤ 4$, remove one coin from $B_k$ and swap
the contents (possibly empty) of the boxes $B_{k+1}$ and $B_{k+2}$.

Determine if there exists a finite sequence of operations of the allowed types, such
that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly
$2010^{2010^{2010}}$ coins.
-/

open Pi Equiv Function

namespace Imo2010P5

/-- The predicate defining states of boxes reachable by the given moves. -/
inductive Reachable : (Fin 6 → ℕ) → Prop
  /-- The starting position with one coin in each box -/
  | base : Reachable 1
  /-- Remove a coin from $B_j$ and add two coins to $B_{j+1}$ -/
  | move1 {B i} (rB : Reachable B) (hi : i < 5) (pB : 0 < B i) :
      Reachable (B - single i 1 + single (i + 1) 2)
  /-- Remove a coin from $B_k$ and swap $B_{k+1}$ and $B_{k+2}$ -/
  | move2 {B i} (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) :
      Reachable (B ∘ swap (i + 1) (i + 2) - single i 1)

/- determine -/ abbrev solution : Bool := sorry

theorem imo2010_p5 : Reachable (single 5 (2010 ^ 2010 ^ 2010)) ↔ solution := sorry

end Imo2010P5

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2010Q5.lean.