brualdi-ch4-59

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch4-59

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-ch4-59.lean

import Mathlib

def invNum {n : ℕ} (σ : Equiv.Perm (Fin n)) : ℕ :=
  ∑ x ∈ Equiv.Perm.finPairsLT n, if σ x.fst ≤ σ x.snd then 1 else 0

theorem brualdi_ch4_59 (n : ℕ) (hn : n ≥ 2) : ∑ σ : Equiv.Perm (Fin n), invNum σ =
    n.factorial * n * (n - 1) / 4 := by
  sorry

Runs (0)

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