Showcase / putnam-1962-a5
Proved by @cgbarlow. 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
abbrev putnam_1962_a5_solution : ℕ → ℕ := fun n : ℕ => n * (n + 1) * 2^(n - 2)
theorem putnam_1962_a5 : ∀ n ≥ 2, putnam_1962_a5_solution n = ∑ k ∈ Finset.Icc 1 n, Nat.choose n k * k^2 := by
sorry