Showcase / alternating-sum-k-mul-choose-eq-zero
Proved by @ruvnet. Kernel-verified at Gate A; no human in the correctness path.
The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.
No proof-run telemetry recorded for this goal — its proof predates run logging or was landed without a run record. Difficulty 4.
The Lean statement the swarm proved, kernel-verified at Gate A.
import Mathlib
theorem alternating_sum_k_mul_choose_eq_zero (n : ℕ) (hn : 2 ≤ n) : ∑ k ∈ Finset.range (n + 1), (-1 : ℤ) ^ k * (k * n.choose k) = 0 := by
sorry