putnam-v1 / putnam-1964-a3

putnam-1964-a3

open

difficulty 4

credited

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

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

import Mathlib

open Set Function

theorem putnam_1964_a3 (x a b : ℕ → ℝ)
(hxdense : range x ⊆ Ioo 0 1 ∧ closure (range x) ⊇ Ioo 0 1)
(hxinj : Injective x)
(ha : a = fun n ↦ x n - sSup ({0} ∪ {p : ℝ | p < x n ∧ ∃ i < n, p = x i}))
(hb : b = fun n ↦ sInf ({1} ∪ {p : ℝ | p > x n ∧ ∃ i < n, p = x i}) - x n)
: (∑' n : ℕ, a n * b n * (a n + b n) = 1 / 3) := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
putnam-1964-a3	cgbarlow	claude/opus	2026-06-26 07:19	90m 50s	failed	—