Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2019P4

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Nat.Factorial.BigOperators
public import Mathlib.Data.Set.Card

public section


open scoped Nat

/-!
# USA Mathematical Olympiad 2019, Problem 4

Let n be a nonnegative integer. Determine the number of ways to choose
sets Sᵢⱼ ⊆ {1, 2, ..., 2n}, for all 0 ≤ i ≤ n and 0 ≤ j ≤ n (not
necessarily distinct), such that

  • |Sᵢⱼ| = i + j, and
  • Sᵢⱼ ⊆ Sₖₗ if 0 ≤ i ≤ k ≤ n and 0 ≤ j ≤ l ≤ n.
-/

namespace Usa2019P4

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

theorem usa2019_p4 (n : ℕ) :
    Nat.card {S : Fin (n + 1) → Fin (n + 1) → Finset (Fin (2 * n)) //
      (∀ i j, (S i j).card = i.val + j.val) ∧
      (∀ i k j l, i ≤ k → j ≤ l → S i j ⊆ S k l)} = answer n := sorry

end Usa2019P4

File author(s): David Renshaw, Kimi K3

This problem has a complete formalized solution.