putnam-v1 / putnam-1970-a1

putnam-1970-a1

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1970-a1

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-1970-a1.lean

import Mathlib

open Metric Set EuclideanGeometry

theorem putnam_1970_a1 (a b : ℝ)
(ha : a > 0)
(hb : b > 0)
(f : ℝ → ℝ)
(f_def : f = fun x : ℝ => Real.exp (a*x) * Real.cos (b*x))
(p : ℕ → ℝ)
(hp : ∃ c : ℝ, c > 0 ∧ ∀ x ∈ ball 0 c, ∑' n : ℕ, (p n)*x^n = f x)
(S : Set ℕ)
(S_def : S = {n : ℕ | p n = 0})
: S = ∅ ∨ ¬Finite S := by
  sorry

Runs (0)

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