Compfiles: Catalog Of Math Problems Formalized In Lean

Bulgaria1998P1

import Mathlib.Tactic

/-!
# Bulgarian Mathematical Olympiad 1998, Problem 1

We will be considering colorings in 2 colors of n (distinct) points
A₁, A₂, ..., Aₙ. Call such a coloring "good" if there exist three points
Aᵢ, Aⱼ, A₂ⱼ₋ᵢ, 1 ≤ i < 2j - i ≤ n, which are colored the same color.

Find the least natural number n (n ≥ 3) such that all colorings
of n points are good.
-/

namespace Bulgaria1998P1

abbrev coloring_is_good {m : ℕ} (color : Set.Icc 1 m → Fin 2) : Prop :=
  ∃ i j : Set.Icc 1 m,
    i < j ∧
    ∃ h3 : 2 * j.val - i ∈ Set.Icc 1 m,
    color i = color j ∧ color i = color ⟨2 * j - i, h3⟩

abbrev all_colorings_are_good (m : ℕ) : Prop :=
  3 ≤ m ∧ ∀ color : Set.Icc 1 m → Fin 2, coloring_is_good color

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

private def check9 (f : Fin 9 → Fin 2) : Bool :=
  (List.finRange 9).any fun i =>
    (List.finRange 9).any fun j =>
      decide (i < j) &&
        if h : 2 * j.val - i.val < 9 then
          decide (f i = f j) && decide (f i = f ⟨2 * j.val - i.val, h⟩)
        else false

private def toFin9 (color : Set.Icc 1 9 → Fin 2) : Fin 9 → Fin 2 :=
  fun i => color ⟨i.val + 1, by constructor <;> omega⟩

private lemma of_check9 (color : Set.Icc 1 9 → Fin 2)
    (h : check9 (toFin9 color) = true) : coloring_is_good color := by
  simp only [check9, toFin9, List.any_eq_true, List.mem_finRange, true_and] at h
  obtain ⟨i, j, hrest⟩ := h
  split at hrest
  case isTrue hk =>
    simp only [Bool.and_eq_true, decide_eq_true_eq] at hrest
    obtain ⟨hij, hcij, hcik⟩ := hrest
    have hmem : 2 * (j.val + 1) - (i.val + 1) ∈ Set.Icc 1 9 := by
      simp only [Set.mem_Icc]; omega
    refine ⟨⟨i.val + 1, by simp only [Set.mem_Icc]; omega⟩,
           ⟨j.val + 1, by simp only [Set.mem_Icc]; omega⟩,
           by simp only [Subtype.mk_lt_mk]; omega, hmem, hcij, ?_⟩
    have heq : 2 * (j.val + 1) - (i.val + 1) = 2 * j.val - i.val + 1 := by omega
    have : (⟨2 * (j.val + 1) - (i.val + 1), hmem⟩ : Set.Icc 1 9) =
           ⟨2 * j.val - i.val + 1, by simp only [Set.mem_Icc]; omega⟩ :=
      Subtype.ext heq
    rw [this]; exact hcik
  case isFalse hk => simp at hrest

theorem bulgaria1998_p1 : IsLeast { m | all_colorings_are_good m } solution_value := sorry


end Bulgaria1998P1

File author(s): David Renshaw

This problem has a complete formalized solution.