Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1999P3

import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1999, Problem 3

Consider an `n × n` square board, where `n` is a fixed even positive integer.
The board is divided into `n^2` unit squares. We say that two different squares on the
board are adjacent if they have a common side.
`N` unit squares on the board are marked in such a way that every square (marked
or unmarked) on the board is adjacent to at least one marked square.
Determine the smallest possible value of `N`.
-/

namespace Imo1999P3

-- 1. Basic Definitions (Visible in Problem Statement)

abbrev Square (n : ℕ) := Fin n × Fin n

/-- Definition of adjacency: Two squares are adjacent if they share a common side. -/
def Adjacent {n : ℕ} (p1 p2 : Square n) : Prop :=
  let (r1, c1) := p1; let (r2, c2) := p2
  ((r1 : ℤ) - r2).natAbs + ((c1 : ℤ) - c2).natAbs = 1

/-- A set s is a valid marking if every square in the grid is adjacent to some square in s. -/
def IsValidMarking {n : ℕ} (s : Finset (Square n)) : Prop :=
  ∀ p : Square n, ∃ m ∈ s, Adjacent p m

/- determine -/ abbrev solution_value (n : ℕ) : ℕ := sorry

theorem imo1999_p3 (n : ℕ) (h_pos : 0 < n) (h_even : Even n) :
  IsLeast
    {k : ℕ | ∃ s : Finset (Square n), IsValidMarking s ∧ s.card = k}
    (solution_value n) := sorry

end Imo1999P3

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

This problem has a complete formalized solution.