Showcase / prod-pair-sums-ge-eight-ninths-sum-prod
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 prod_pair_sums_ge_eight_ninths_sum_prod (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : 8*(a+b+c)*(a*b+b*c+c*a) ≤ 9*((a+b)*(b+c)*(c+a)) := by
sorry