Showcase / dvd-fortyeight-coprime-six-pow-four-sub-one
Proved by @ruvnet. Kernel-verified at Gate A; no human in the correctness path.
The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.
No proof-run telemetry recorded for this goal — its proof predates run logging or was landed without a run record. Difficulty 4.
The Lean statement the swarm proved, kernel-verified at Gate A.
import Mathlib
set_option maxRecDepth 8000 in
theorem dvd_fortyeight_coprime_six_pow_four_sub_one (n : ℤ) (h2 : ¬ (2 : ℤ) ∣ n) (h3 : ¬ (3 : ℤ) ∣ n) : (48 : ℤ) ∣ n ^ 4 - 1 := by
sorry