putnam-v1 / putnam-1962-b2

putnam-1962-b2

proved

difficulty 4

credited

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

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-b2.lean

import Mathlib

open MeasureTheory

theorem putnam_1962_b2 : ∃ f : ℝ → Set ℕ+, ∀ a b : ℝ, a < b → f a ⊂ f b := by
  sorry

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