Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2025P6

import Mathlib.Analysis.MeanInequalities
import Archive.Wiedijk100Theorems.AscendingDescendingSequences

/-!
# International Mathematical Olympiad 2025, Problem 6

Consider a 2025 × 2025 grid of unit squares. Matilda wishes to place
on the grid some rectangular tiles, possibly of different sizes,
such that each side of every tile lies on a grid line and
every unit square is covered by at most one tile.
Determine the minimum number of tiles Matilda needs to place
so that each row and each column of the grid has exactly one unit square
that is not covered by any tile.
-/

namespace Imo2025P6

variable {n : ℕ}
abbrev Point (n : ℕ) := Fin n × Fin n
variable {all_black : Finset (Point n)}

section ProblemSetup
variable [NeZero n]
abbrev px (p : Point n) : ℕ := p.1.val
abbrev py (p : Point n) : ℕ := p.2.val

structure Matilda (n : ℕ) [NeZero n] (all_black : Finset (Point n)) where
  x_min : ℕ
  x_max : ℕ
  y_min : ℕ
  y_max : ℕ
  h_x_le : x_min ≤ x_max
  h_y_le : y_min ≤ y_max
  h_x_bound : x_max < n
  h_y_bound : y_max < n
  h_disjoint : ∀ p ∈ all_black, ¬(x_min ≤ px p ∧ px p ≤ x_max ∧ y_min ≤ py p ∧ py p ≤ y_max)
@[simp]
def Matilda.mem (m : Matilda n all_black) (p : Point n) : Prop :=
  m.x_min ≤ px p ∧ px p ≤ m.x_max ∧ m.y_min ≤ py p ∧ py p ≤ m.y_max

def IsValidConfiguration (n : ℕ) [NeZero n]
  (all_black : Finset (Point n)) (partition : Finset (Matilda n all_black)) : Prop :=
  all_black.card = n ∧
  (∀ p ∈ all_black, ∀ q ∈ all_black, px p = px q → p = q) ∧
  (∀ p ∈ all_black, ∀ q ∈ all_black, py p = py q → p = q) ∧
  (∀ p : Point n, p ∉ all_black → ∃! m ∈ partition, m.mem p)

def IsMinMatildaCount (n : ℕ) [NeZero n] (m : ℕ) : Prop :=
  (∀ (all_black : Finset (Point n)) (partition : Finset (Matilda n all_black)),
      IsValidConfiguration n all_black partition → m ≤ partition.card) ∧
  (∃ (all_black : Finset (Point n)) (partition : Finset (Matilda n all_black)),
      IsValidConfiguration n all_black partition ∧ partition.card = m)

end ProblemSetup

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

theorem imo2025_p6 : IsMinMatildaCount 2025  solution_value := sorry

end Imo2025P6

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

This problem has a complete formalized solution.