imo-v1 / imo2021p2
imo2021p2
open
difficulty 4
credited
Run this goal:
./swarm/run.sh --goal imo2021p2What 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/imo2021p2.lean
import Mathlib
theorem imo2021p2 {n : ℕ} (x : Fin n → ℝ) : ∑ i, ∑ j, √|x i - x j| ≤ ∑ i, ∑ j, √|x i + x j| := by
sorryRuns (0)
No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.