brualdi-ch7-27

open

difficulty 4

credited

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

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-27.lean

import Mathlib

abbrev S (n : ℕ) : Finset ℕ :=
  {m < 10^n | (Nat.digits 10 m).length = n ∧
  (∀ i : Fin (Nat.digits 10 m).length, Odd ((Nat.digits 10 m).get i)) ∧
  Even ((Nat.digits 10 m).count 1) ∧ Even ((Nat.digits 10 m).count 3) ∧
  ((Nat.digits 10 m).count 1) ≠ 0 ∧ ((Nat.digits 10 m).count 3) ≠ 0}

theorem brualdi_ch7_27 (n : ℕ) : (S n).card = ((fun n => (5 ^ n - 4 ^ (n + 1) + 6 * 3 ^ n - 4 * 2 ^ n + 1) / 4 ) : ℕ → ℕ ) n := by
  sorry

Runs (0)

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