putnam-1966-a6

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.

import Mathlib

open Topology Filter

theorem putnam_1966_a6 (a : ℕ → (ℕ → ℝ))
(ha : ∀ n ≥ 1, a n n = n ∧ ∀ m ≥ 1, m < n → a n m = m * Real.sqrt (1 + a n (m + 1)))
: Tendsto (fun n => a n 1) atTop (𝓝 3) := by
  sorry

The swarm split this goal into helper sub-lemmas, proved them separately, and composed them back into the parent proof (unsorry ADR-009). Decomposed by afnz-zbook-b336.

• putnam-1966-a6-s1

  open

  Open — not yet proved.

• putnam-1966-a6-s2

  open

  Open — not yet proved.

• putnam-1966-a6-s3

  open

  Open — not yet proved.

• putnam-1966-a6-s4

  open

  Open — not yet proved.

Runs (1)