Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2001P4

import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.GroupTheory.Perm.Fin

/-!
# International Mathematical Olympiad 2001, Problem 4

Let $n > 1$ be an odd integer and let $c_1, c_2, \dots, c_n$ be integers. For
each permutation $a = (a_1, a_2, \dots, a_n)$ of $\{1, 2, \dots, n\}$, define
$S(a) = \sum_{i=1}^n c_i a_i$. Prove that there exist two permutations
$a ≠ b$ of $\{1, 2, \dots, n\}$ such that $n!$ is a divisor of $S(a) - S(b)$.
-/

namespace Imo2001Q4

open Equiv Finset
open scoped Nat

variable {n : ℕ} {c : Fin n → ℤ}

/-- The function `S` in the problem. As implemented here it accepts a
permutation of `Fin n` rather than `Icc 1 n`, and as such contains `+ 1`
to compensate. -/
def S (c : Fin n → ℤ) (a : Perm (Fin n)) : ℤ := ∑ i, c i * (a i + 1)

theorem imo2001_p4 (hn : Odd n ∧ 1 < n) :
    ∃ a b, a ≠ b ∧ (n ! : ℤ) ∣ S c a - S c b := sorry

end Imo2001Q4

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4.