Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2000P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2000, Problem 4

Find the smallest positive integer $n$ such that if $n$ squares of a
$1000 \times 1000$ chessboard are colored, then there will exist three
colored squares whose centers form a right triangle with sides parallel
to the edges of the board.
-/

namespace Usa2000P4

/-- A set `S` of squares on an `m × n` board contains no forbidden triangle:
one cannot find three (distinct) chosen squares whose centers form a right
triangle with sides parallel to the edges of the board, that is, with two of
them in the same row and two of them in the same column. -/
def Good {m n : ℕ} (S : Finset (Fin m × Fin n)) : Prop :=
  ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x ≠ y → y ≠ z → x ≠ z →
    ¬((x.1 = y.1 ∨ x.1 = z.1 ∨ y.1 = z.1) ∧ (x.2 = y.2 ∨ x.2 = z.2 ∨ y.2 = z.2))

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

theorem usa2000_p4 :
    IsLeast {n : ℕ | ∀ S : Finset (Fin 1000 × Fin 1000), S.card = n → ¬Good S}
      smallestN := sorry

end Usa2000P4

File author(s): Kimi K3

This problem has a complete formalized solution.