putnam-v1 / putnam-1962-b3

putnam-1962-b3

proved

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1962-b3

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/putnam-1962-b3.lean

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

Runs (0)

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