Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2010P6

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Field.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Finset.Sort
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2010, Problem 6

There are 68 ordered pairs (not necessarily distinct) of nonzero integers
on a blackboard. It's known that for no integer k does both (k, k) and
(−k, −k) appear. A student erases some of the 136 integers such that no two
erased integers have sum zero, and scores one point for each ordered pair
with at least one erased integer. What is the maximum possible score the
student can guarantee?
-/

namespace Usa2010P6

/-- A choice of integers to erase is valid if no two erased integers sum to zero.
(If a value `x` is erased at some position, erasing every occurrence of `x` is never
worse, so the optimal strategies correspond exactly to sets of values `T` with
`x ∈ T → -x ∉ T`.) -/
def ValidErase (T : Finset ℤ) : Prop := ∀ x ∈ T, -x ∉ T

/-- The score obtained by erasing the set `T` from the board `L`:
one point for each ordered pair with at least one erased entry. -/
def score (L : List (ℤ × ℤ)) (T : Finset ℤ) : ℕ :=
  (L.filter (fun p => decide (p.1 ∈ T ∨ p.2 ∈ T))).length

/-- A valid board: 68 ordered pairs of nonzero integers such that for no `k`
do both `(k, k)` and `(-k, -k)` appear. -/
structure ValidBoard (L : List (ℤ × ℤ)) : Prop where
  length_eq : L.length = 68
  nonzero : ∀ p ∈ L, p.1 ≠ 0 ∧ p.2 ≠ 0
  no_both_loops : ∀ k : ℤ, (k, k) ∈ L → (-k, -k) ∉ L

/-- The maximum score the student can guarantee. -/
/- determine -/ abbrev N : ℕ := sorry

theorem usa2010_p6 :
    IsGreatest {m : ℕ | ∀ L : List (ℤ × ℤ), ValidBoard L →
      ∃ T : Finset ℤ, ValidErase T ∧ m ≤ score L T} N := sorry

end Usa2010P6

File author(s): Kimi K3

This problem has a complete formalized solution.