Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1999P1

module

public import Batteries.Data.List.Basic
public import Mathlib.Data.Finset.Basic
public import Mathlib.Data.Finset.Card
public import Mathlib.Data.Fintype.BigOperators
public import Mathlib.Data.Fintype.Prod
public import Mathlib.Data.List.Chain
public import Mathlib.Combinatorics.SimpleGraph.Acyclic
public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Combinatorics.SimpleGraph.Hasse
public import Mathlib.Tactic.Linarith

public section


/-!
USA Mathematical Olympiad 1999, Problem 1

Some checkers placed on an n × n checkerboard satisfy the following conditions:
 a. every square that does not contain a checker shares a side with one that does;
 b. given any pair of squares that contain checkers, there is a sequence of squares
    containing checkers, starting and ending with the given squares, such that
    every two consecutive squares of the sequence share a side.

Prove that at least (n²-2)/3 checkers have been placed on the board.
-/

namespace Usa1999P1

def checkerboard (n : ℕ) := Fin n × Fin n

def adjacent {n : ℕ} : checkerboard n → checkerboard n → Prop
| ⟨a1, a2⟩, ⟨b1, b2⟩ =>
  (a1.val = b1.val ∧ a2.val = b2.val + 1) ∨
  (a1.val = b1.val ∧ a2.val + 1 = b2.val) ∨
  (a2.val = b2.val ∧ a1.val = b1.val + 1) ∨
  (a2.val = b2.val ∧ a1.val + 1 = b1.val )

theorem usa1999_p1 (n : ℕ) (c : Finset (checkerboard n))
    (ha : ∀ x : checkerboard n, x ∈ c ∨ (∃ y ∈ c, adjacent x y))
    (hb : ∀ x ∈ c, ∀ y ∈ c,
      ∃ p : List (checkerboard n),
        (∀ z, z ∈ p → z ∈ c) ∧
        List.IsChain adjacent p ∧
        List.head? p = x ∧
        List.getLast? p = y) :
    n^2 ≤ c.card * 3 + 2 := sorry


end Usa1999P1

File author(s): David Renshaw

This problem has a complete formalized solution.