putnam-v1 / putnam-1968-b1

putnam-1968-b1

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1968-b1

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-1968-b1.lean

import Mathlib

open MeasureTheory
open scoped ProbabilityTheory
abbrev putnam_1968_b1_solution : ℝ → ℝ → ℝ → ℝ := fun a b c => a + b - c

theorem putnam_1968_b1 {Ω : Type*}
    [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)]
    (X Y : Ω → ℤ)
    (hX : Measurable X)
    (hY : Measurable Y)
    (hX' : Set.Finite (X '' Set.univ))
    (hY' : Set.Finite (Y '' Set.univ))
    (k : ℤ) :
    (ℙ {ω : Ω | min (X ω) (Y ω) = k}).toReal =
      putnam_1968_b1_solution (ℙ (X⁻¹' {k})).toReal (ℙ (Y⁻¹' {k})).toReal
      (ℙ {ω : Ω | max (X ω) (Y ω) = k}).toReal := by
  sorry

Runs (0)

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