brualdi-ch2-6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch2-6

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-ch2-6.lean

import Mathlib

theorem brualdi_ch2_6 (s : Finset ℕ)
    (hs : ∀ n, n ∈ s ↔ n > 5400 ∧ (Nat.digits 10 n).Nodup ∧ 2 ∉ (Nat.digits 10 n) ∧ 7 ∉ (Nat.digits 10 n)) :
    s.card = ((94830) : ℕ ) := by
  sorry

Runs (0)

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