Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2016P1

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fin.VecNotation
public import Mathlib.Data.Fintype.Powerset

public section


/-!
# USA Mathematical Olympiad 2016, Problem 1

Let X₁, X₂, …, X₁₀₀ be a sequence of mutually distinct nonempty subsets of a set S.
Any two sets Xᵢ and Xᵢ₊₁ are disjoint and their union is not the whole set S,
that is, Xᵢ ∩ Xᵢ₊₁ = ∅ and Xᵢ ∪ Xᵢ₊₁ ≠ S, for all i ∈ {1, …, 99}.
Find the smallest possible number of elements in S.
-/

namespace Usa2016P1

open Finset

/-- `HasChain n` means that an `n`-element set (which we may take to be `Fin n`)
admits a sequence of 100 mutually distinct nonempty subsets in which any two
consecutive sets are disjoint and do not cover the whole set. -/
def HasChain (n : ℕ) : Prop :=
  ∃ X : Fin 100 → Finset (Fin n),
    (∀ i, (X i).Nonempty) ∧
      (∀ i j, X i = X j → i = j) ∧
        ∀ i : Fin 99, Disjoint (X i.castSucc) (X i.succ) ∧
          X i.castSucc ∪ X i.succ ≠ univ

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

theorem usa2016_p1 : IsLeast {n | HasChain n} solution_value := sorry

end Usa2016P1

File author(s): Kimi K3

This problem has a complete formalized solution.