putnam-v1 / putnam-1962-b1

putnam-1962-b1

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1962-b1

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/putnam-1962-b1.lean

import Mathlib

theorem putnam_1962_b1 (p : ℕ → ℝ → ℝ)
(x y : ℝ)
(n : ℕ)
(h0 : p 0 = fun x : ℝ => 1)
(hp : ∀ n > 0, p n = fun x : ℝ => ∏ i ∈ Finset.range n, (x - i))
: p n (x+y) = ∑ k ∈ Finset.range (n+1), Nat.choose n k * (p k x) * (p (n - k) y) := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.