brualdi-ch7-15

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch7-15

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-ch7-15.lean

import Mathlib

theorem brualdi_ch7_15 : PowerSeries.mk (fun (n : ℕ) => (n : ℝ) ^ 3) = ((PowerSeries.X * (PowerSeries.X ^ 2 + 4 * PowerSeries.X + 1) * PowerSeries.inv (1 - PowerSeries.X) ^ 4) : PowerSeries ℝ ) := by
  sorry

Runs (0)

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