putnam-v1 / putnam-1964-a2

putnam-1964-a2

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1964-a2

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-1964-a2.lean

import Mathlib

open Set
abbrev putnam_1964_a2_solution : ℝ → Set (ℝ → ℝ) := fun _ ↦ ∅

theorem putnam_1964_a2 (α : ℝ)
: (putnam_1964_a2_solution α = {f : ℝ → ℝ | (∀ x ∈ Icc 0 1, f x > 0) ∧ ContinuousOn f (Icc 0 1) ∧ ∫ x in (0)..1, f x = 1 ∧ ∫ x in (0)..1, x * f x = α ∧ ∫ x in (0)..1, x^2 * f x = α^2}) := by
  sorry

Runs (0)

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