Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2025P5

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Data.Nat.Factorial.BigOperators
public import Mathlib.Data.Nat.Factorization.Basic
public import Mathlib.Data.Nat.GCD.BigOperators
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas

public section


/-!
# USA Mathematical Olympiad 2025, Problem 5

Find all positive integers $k$ such that: for every positive integer $n$, the sum
$$\binom{n}{0}^k + \binom{n}{1}^k + \cdots + \binom{n}{n}^k$$
is divisible by $n + 1$.
-/

namespace Usa2025P5

open Finset
open scoped Nat

/- determine -/ abbrev solution_set : Set ℕ := sorry

theorem usa2025_p5 (k : ℕ) (hk : 0 < k) :
    k ∈ solution_set ↔ ∀ n : ℕ, 0 < n → (n + 1) ∣ ∑ i ∈ range (n + 1), (n.choose i) ^ k := sorry

end Usa2025P5

File author(s): Kimi K3

This problem has a complete formalized solution.