`Compfiles/Usa2025P5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

10 declarations, 0 contain sorry, 0 declared as axioms

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$.

Imports (7)

Imported by 1 file

Compfiles.lean

determine Usa2025P5.solution_set line 34 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Even
1 instances, coercions and auxiliary constants left out.
lemma Usa2025P5.sum_range_mul Split a sum over range (p * M) into M blocks of p consecutive terms line 53 source
Source documentation
Split a sum over range (p * M) into M blocks of p consecutive terms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Eq, Finset.sum, Finset.range, HMul.hMul, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Finset, MulZeroClass.mul_zero, eq_self, Eq.mpr, id, Nat.succ, Nat.mul_succ, Finset.sum_range_add, Finset.sum_range_succ, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_mul {M' : Type*} [AddCommMonoid M'] (f : ℕ → M') (p M : ℕ) :
    ∑ i ∈ range (p * M), f i = ∑ m ∈ range M, ∑ r ∈ range p, f (p * m + r) := by
…
```
Mentions: f
lemma Usa2025P5.filter_dvd_succ_range The elements j of range i with p ∣ j + 1 are exactly the numbers p * (ℓ + 1) - 1 with ℓ ∈ range (i / p) line 61 source
Source documentation
The elements j of range i with p ∣ j + 1 are exactly the numbers p * (ℓ + 1) - 1 with ℓ ∈ range (i / p).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Finset, Finset.filter, Dvd.dvd, HAdd.hAdd, Finset.range, Finset.image, HSub.hSub, HMul.hMul, HDiv.hDiv
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Exists, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, LE.le, GT.gt, Or, Nat.eq_zero_or_pos, absurd, Eq.mp, MulZeroClass.mul_zero and 17 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma filter_dvd_succ_range (p i : ℕ) (hp : 0 < p) :
    (range i).filter (fun j => p ∣ j + 1)
      = (range (i / p)).image (fun ℓ => p * (ℓ + 1) - 1) := by
…
```
lemma Usa2025P5.injOn_mul_succ_sub_one The map ℓ ↦ p * (ℓ + 1) - 1 is injective on range M line 93 source
Source documentation
The map ℓ ↦ p * (ℓ + 1) - 1 is injective on range M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Set.InjOn, HSub.hSub, HMul.hMul, HAdd.hAdd, Finset, Finset.range
Proof uses: Membership.mem, Set, Eq, Nat.mul_pos, Nat.succ_pos, Nat.mul_left_cancel
23 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma injOn_mul_succ_sub_one (p M : ℕ) (hp : 0 < p) :
    Set.InjOn (fun ℓ => p * (ℓ + 1) - 1) ↑(range M) := by
…
```
lemma Usa2025P5.choose_mul_prod_filter_eq Splitting `n.choose i * (i)! line 107 source
Source documentation
Splitting n.choose i * (i)! = ∏ j ∈ range i, (n - j) into the factors with p ∣ j + 1 and those with p ∤ j + 1, and cancelling the common factor p ^ (i / p) * (i / p)!, gives n.choose i * P = (M - 1).choose (i / p) * R, where P = ∏ j, (j + 1) and R = ∏ j, (n - j) are the products over the j < i with p ∤ j + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, LE.le, Nat.choose, Finset.prod, Finset.filter, Not, Dvd.dvd, Finset.range, HSub.hSub, HDiv.hDiv
Proof uses: Eq.mpr, Finset.image, id, congrArg, Finset, Usa2025P5.filter_dvd_succ_range, Finset.prod_image, Usa2025P5.injOn_mul_succ_sub_one, Eq.refl, Nat.factorial, Nat.descFactorial, Nat.descFactorial_eq_factorial_mul_choose, Eq.mp, Nat.descFactorial_eq_prod_range, mul_comm, Nat.factorial_eq_prod_range_add_one, Finset.prod_filter_mul_prod_filter_not, HPow.hPow, Trans.simple, Finset.prod_congr and 47 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma choose_mul_prod_filter_eq {p n M i : ℕ} (hp : 0 < p) (hM : p * M = n + 1) (hi : i ≤ n) :
    n.choose i * ∏ j ∈ (range i).filter (fun j => ¬ p ∣ j + 1), (j + 1)
      = (M - 1).choose (i / p) * ∏ j ∈ (range i).filter (fun j => ¬ p ∣ j + 1), (n - j) := by
…
```
lemma Usa2025P5.choose_cast_zmod The key congruence: if the prime power p ^ e divides n + 1 and p * M = n + 1, then n.choose i ≡ (-1) ^ (i - i / p) * (M - 1).choose (i / p) modulo p ^ e line 169 source
Source documentation
The key congruence: if the prime power p ^ e divides n + 1 and p * M = n + 1, then n.choose i ≡ (-1) ^ (i - i / p) * (M - 1).choose (i / p) modulo p ^ e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, Eq, HMul.hMul, ZMod, Nat.choose, Neg.neg, HSub.hSub, HDiv.hDiv
Proof uses: Iff.mpr, ZMod.natCast_eq_zero_iff, Finset.prod, Finset.filter, Not, Finset.range, Usa2025P5.choose_mul_prod_filter_eq, Nat.Prime.pos, Finset.card, Finset.card_filter_add_card_filter_not, Eq.mp, congrArg, Nat.card_multiples, Finset.card_range, Membership.mem, Finset, le_trans, Nat.le_of_lt, Iff.mp, LT.lt and 79 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma choose_cast_zmod {p e n M i : ℕ} (hp : p.Prime) (he : 1 ≤ e) (hdvd : p ^ e ∣ n + 1)
    (hM : p * M = n + 1) (hi : i ≤ n) :
    ((n.choose i : ℕ) : ZMod (p ^ e))
      = (-1) ^ (i - i / p) * (((M - 1).choose (i / p) : ℕ) : ZMod (p ^ e)) := by
…
```
lemma Usa2025P5.sum_modEq Documented declaration: sum_modEq line 221 source
Source documentation
Summing the key congruence over blocks of p consecutive indices: if k is even, p ^ e ∣ n + 1 and p * M = n + 1, then ∑ i, (n.choose i) ^ k ≡ p * ∑ m, ((M - 1).choose m) ^ k modulo p ^ e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, Even, Eq, HMul.hMul, Nat.ModEq, Finset.sum, Finset.range, Nat.choose, HSub.hSub
Proof uses: Eq.mpr, ZMod, id, congrArg, Eq.symm, propext, ZMod.natCast_eq_natCast_iff, congr, Eq.trans, Nat.cast_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.cast_pow, Nat.cast_mul, Trans.trans, Usa2025P5.sum_range_mul, rfl, mul_le_mul_right and 24 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma sum_modEq {p e n M k : ℕ} (hp : p.Prime) (he : 1 ≤ e) (hdvd : p ^ e ∣ n + 1)
    (hk : Even k) (hM : p * M = n + 1) :
    (∑ i ∈ range (n + 1), (n.choose i) ^ k)
      ≡ p * (∑ m ∈ range M, ((M - 1).choose m) ^ k) [MOD p ^ e] := by
…
```
lemma Usa2025P5.dvd_sum_of_even Sufficiency: for even k, n + 1 divides ∑ i ∈ range (n + 1), (n.choose i) ^ k for every positive n line 266 source
Source documentation
Sufficiency: for even k, n + 1 divides ∑ i ∈ range (n + 1), (n.choose i) ^ k for every positive n. Proof by strong induction on n: for each prime p with p ^ e exactly dividing n + 1, sum_modEq reduces the claim modulo p ^ e to the induction hypothesis at M - 1, where p * M = n + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Even, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, Nat.choose
Proof uses: Nat.strong_induction_on, Ne, Eq, Eq.mpr, id, congrArg, Nat.choose_zero_right, one_pow, Eq.refl, LE.le, Finset.single_le_sum, Membership.mem, Finset, Nat.zero_le, Iff.mpr, Finset.mem_range, Finsupp, Nat.factorization, Eq.symm, propext and 41 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_sum_of_even {k : ℕ} (hk : Even k) (n : ℕ) :
    0 < n → (n + 1) ∣ ∑ i ∈ range (n + 1), (n.choose i) ^ k := by
…
```
lemma Usa2025P5.even_of_dvd Necessity: taking n = 2, the divisibility 3 ∣ 2 + 2 ^ k forces k to be even line 325 source
Source documentation
Necessity: taking n = 2, the divisibility 3 ∣ 2 + 2 ^ k forces k to be even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, Nat.choose, Even
Proof uses: Decidable.byContradiction, Not, Eq, Finset.sum_range_zero, Finset.sum_range_one, Eq.mpr, id, congrArg, rfl, Finset.sum_range_succ, Eq.refl, Nat.choose_zero_right, Nat.choose_one_right, Nat.choose_self, one_pow, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos and 39 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma even_of_dvd {k : ℕ}
    (h : ∀ n : ℕ, 0 < n → (n + 1) ∣ ∑ i ∈ range (n + 1), (n.choose i) ^ k) :
    Even k := by
…
```
Mentions: h
problem Usa2025P5.usa2025_p5 line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Usa2025P5.solution_set, Dvd.dvd, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, Nat.choose
Proof uses: Iff.intro, Usa2025P5.dvd_sum_of_even, Usa2025P5.even_of_dvd
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.