Showcase / putnam-1962-b3
Proved by @cgbarlow. 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
open MeasureTheory
theorem putnam_1962_b3 (S : Set (EuclideanSpace ℝ (Fin 2)))
(hS : Convex ℝ S ∧ 0 ∈ S)
(htopo : (0 ∈ interior S) ∨ IsClosed S)
(hray : ∀ P : EuclideanSpace ℝ (Fin 2), P ≠ 0 → ∃ Q : EuclideanSpace ℝ (Fin 2), SameRay ℝ P Q ∧ Q ∉ S)
: Bornology.IsBounded S := by
sorry