Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2009P2

module

public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Interval
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2009, Problem 2

Let n be a positive integer. Determine the size of the largest subset of
{−n, −n+1, ..., n−1, n} which does not contain three elements a, b, c
(not necessarily distinct) satisfying a + b + c = 0.
-/

namespace Usa2009P2

/-- A set of integers is called *good* if it does not contain three elements
`a`, `b`, `c` (not necessarily distinct) satisfying `a + b + c = 0`. -/
abbrev IsGood (A : Finset ℤ) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a + b + c ≠ 0

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

theorem usa2009_p2 (n : ℕ) (hn : 0 < n) :
    IsGreatest
      {k : ℕ | ∃ A : Finset ℤ,
        A ⊆ Finset.Icc (-(n : ℤ)) (n : ℤ) ∧ IsGood A ∧ A.card = k}
      (answer n) := sorry

end Usa2009P2

File author(s): Kimi K3

This problem has a complete formalized solution.