Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1986P3

import Mathlib.Data.Fin.Basic
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1986, Problem 3

To each vertex of a regular pentagon, an integer is assigned,
in such a way that the sum of all five numbers is positive.
If three consecutive vertices are assigned the numbers $x, y, z$ respectively and $y < 0$,
then the following operation is allowed: $x, y, z$ are replaced by $x+y, -y, z+y$ respectively.
Such an operation is performed repeatedly as long as at least one of the five numbers is negative.
Determine whether this procedure necessarily comes to an end after a finite number of steps.
-/

namespace Imo1986P3

open BigOperators

/-- State of the pentagon: an integer assigned to each vertex. -/
def State := Fin 5 → ℤ

/-- The sum of all integers on the pentagon. -/
def State.sum (s : State) : ℤ := ∑ i : Fin 5, s i

/-- The operation performed at vertex `i` when `s i < 0`. -/
def move (s : State) (i : Fin 5) : State :=
  fun j =>
    if j == i - 1 then s (i - 1) + s i
    else if j == i     then -s i
    else if j == i + 1 then s (i + 1) + s i
    else s j

/--
The transition relation `Step next current` asserts that `next` is obtained
from `current` by applying the move operation at some vertex `i` where `s i < 0`.
The order of arguments `(next current)` is chosen to match the convention of `Acc`.
-/
def Step (next current : State) : Prop :=
  ∃ i : Fin 5, current i < 0 ∧ next = move current i

/--
Main Theorem: IMO 1986 Problem 3.
Starting from any state with a positive sum, the process terminates.
-/
theorem imo1986_p3 (s₀ : State) (h_sum : 0 < s₀.sum) :
    Acc Step s₀ := sorry

end Imo1986P3

File author(s): lean-tom (with assistance from Gemini)

This problem has a complete formalized solution.