combibench-v1 / brualdi-ch7-7
brualdi-ch7-7
open
difficulty 4
credited
Run this goal:
./swarm/run.sh --goal brualdi-ch7-7What 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-7.lean
import Mathlib
theorem brualdi_ch7_7 (m n d : ℕ+) (hmd : d = Nat.gcd m n) :
Nat.gcd (Nat.fib m) (Nat.fib n) = Nat.fib d := by
sorryRuns (0)
No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.