brualdi-ch5-9

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch5-9

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/brualdi-ch5-9.lean

import Mathlib

theorem brualdi_ch5_9 (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (-1 : ℤ) ^ k * (n.choose k) * 10 ^ k =
    ((fun n => (-9 : ℤ)^n) : ℕ → ℤ ) n := by
  sorry

Runs (0)

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