putnam-v1 / putnam-1969-b5

putnam-1969-b5

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1969-b5

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-1969-b5.lean

import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b5 (a : ℕ → ℝ)
(ha : StrictMono a ∧ (∀ x : ℕ, a x > 0))
(hinvasum : ∃ C : ℝ, Tendsto (fun n => ∑ i : Fin n, 1/(a i)) atTop (𝓝 C))
(k : ℝ → ℕ)
(hk : k = fun x => {n | a n ≤ x}.ncard)
: Tendsto (fun t => (k t)/t) atTop (𝓝 0) := by
  sorry

Runs (0)

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