putnam-v1 / putnam-1962-b6

putnam-1962-b6

open

difficulty 4

credited

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

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

import Mathlib

open Real

theorem putnam_1962_b6 (n : ℕ)
(a b : ℕ → ℝ)
(xs : Set ℝ)
(f : ℝ → ℝ)
(hf : f = fun x : ℝ => ∑ k ∈ Finset.Icc 0 n, ((a k) * Real.sin (k * x) + (b k) * Real.cos (k * x)))
(hf1 : ∀ x ∈ Set.Icc 0 (2 * π), |f x| ≤ 1)
(hxs : xs.ncard = 2 * n ∧ xs ⊆ Set.Ico 0 (2 * π))
(hfxs : ∀ x ∈ xs, |f x| = 1)
: (¬∃ c : ℝ, f = fun x : ℝ => c) → ∃ a : ℝ, f = fun x : ℝ => Real.cos (n * x + a) := by
  sorry

Runs (0)

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