Showcase / platonic-schlafli-core
Attribution inferred from git history (no explicit solver credit). 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
theorem platonic_schlafli_pairs (p q : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q) (h : (p : ℚ)⁻¹ + (q : ℚ)⁻¹ > 2⁻¹) : (p, q) ∈ ({(3,3),(3,4),(4,3),(3,5),(5,3)} : Finset (ℕ × ℕ)) := by
sorry