Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2016P2

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Choose.Factorization

public section


/-!
USA Mathematical Olympiad 2016, Problem 2

Prove that for any positive integer k,

  (k²)! · ∏_{j=0}^{k-1} j!/(j + k)!

is an integer.
-/

namespace Usa2016P2

open Finset
open scoped Nat

theorem usa2016_p2 (k : ℕ) (hk : 0 < k) :
    (∏ j ∈ Finset.range k, (j + k) !) ∣ (k ^ 2) ! * ∏ j ∈ Finset.range k, j ! := sorry

end Usa2016P2

File author(s): Kimi K3

This problem has a complete formalized solution.