Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2000P4

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fin.VecNotation
public import Mathlib.Data.Fintype.Perm
public import Mathlib.Order.CompletePartialOrder
public import Mathlib.Tactic.IntervalCases

public section


/-!
# International Mathematical Olympiad 2000, Problem 4

100 cards are numbered 1 to 100 (each card different) and placed in 3 boxes
(at least one card in each box). How many ways can this be done so that if
two boxes are selected and a card is taken from each, then the knowledge of
their sum alone is always sufficient to identify the third box?
-/

namespace Imo2000P4

/-- A placement of the 100 cards into 3 boxes (labeled by `ZMod 3`) is *valid*
if every box is nonempty and whenever two boxes are selected and a card is
taken from each, the sum of the two drawn cards always suffices to identify
the third box: any two such selections of two distinct boxes and two cards
with the same sum leave the same box unselected.
Card `i + 1` is represented by the index `i : Fin 100`. -/
def ValidPlacement (f : Fin 100 → ZMod 3) : Prop :=
  Function.Surjective f ∧
  ∀ i j k l : Fin 100, f i ≠ f j → f k ≠ f l →
    (i : ℕ) + 1 + ((j : ℕ) + 1) = (k : ℕ) + 1 + ((l : ℕ) + 1) →
    ∀ b : ZMod 3, (b ≠ f i ∧ b ≠ f j) ↔ (b ≠ f k ∧ b ≠ f l)

/- determine -/ abbrev solution_value : ℕ := sorry

theorem imo2000_p4 :
    {g : Fin 100 → ZMod 3 | ValidPlacement g}.ncard = solution_value := sorry

end Imo2000P4

File author(s): Kimi K3

This problem has a complete formalized solution.