Showcase / no-nat-sq-eq-two-mul-sq
Proved by @perttu. 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.
The Lean statement the swarm proved, kernel-verified at Gate A.
import Mathlib
theorem no_nat_sq_eq_two_mul_sq : ¬ ∃ a b : ℕ, 0 < b ∧ a ^ 2 = 2 * b ^ 2 := by
sorry