putnam-v1 / putnam-1969-b3

putnam-1969-b3

open

difficulty 4

credited

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

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

import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_b3 (T : ℕ → ℝ)
(hT1 : ∀ n : ℕ, n ≥ 1 → (T n) * (T (n + 1)) = n)
(hT2 : Tendsto (fun n => (T n)/(T (n + 1))) atTop (𝓝 1))
: Real.pi * (T 1)^2 = 2 := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
putnam-1969-b3	cgbarlow	claude/opus	2026-06-26 16:04	20m 56s	failed	—