brualdi-ch3-18

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch3-18

What 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/brualdi-ch3-18.lean

import Mathlib

theorem brualdi_ch3_18 (points : Fin 5 → (EuclideanSpace ℝ (Fin 2)))
    (h_points : ∀ i, 0 ≤ ((points i) 0) ∧ ((points i) 0) ≤ 2 ∧ 0 ≤ ((points i) 1) ∧ ((points i) 1) ≤ 2) :
    ∃ i j, i ≠ j ∧ dist (points i) (points j) ≤ √2 := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.