Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2003P6

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Nat.Dist
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2003, Problem 6

At the vertices of a regular hexagon are written six nonnegative integers
whose sum is 2003^2003. Bert is allowed to make moves of the following form:
he may pick a vertex and replace the number written there by the absolute
value of the difference between the numbers written at the two neighboring
vertices. Prove that Bert can make a sequence of moves, after which the
number 0 appears at all six vertices.
-/

namespace Usa2003P6

theorem usa2003_p6 (f : ZMod 6 → ℕ) (hsum : ∑ i, f i = 2003 ^ 2003) :
    ∃ l : List (ZMod 6),
      l.foldl (fun g j => Function.update g j (Nat.dist (g (j - 1)) (g (j + 1)))) f = 0 := sorry

end Usa2003P6

File author(s): Kimi K3

This problem has a complete formalized solution.