putnam-v1 / putnam-1964-a5

putnam-1964-a5

open

difficulty 4

credited

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

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

import Mathlib

open Set Function Filter Topology

theorem putnam_1964_a5 (pa : (ℕ → ℝ) → Prop)
    (hpa : ∀ a, pa a ↔ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n ∈ Finset.range N, 1 / a n) atTop (𝓝 L)) :
    ∃ k : ℝ, ∀ a : ℕ → ℝ, pa a →
      ∑' n : ℕ, (n + 1) / (∑ i ∈ Finset.range (n + 1), a i) ≤ k * ∑' n : ℕ, 1 / a n := by
  sorry

Runs (0)

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