putnam-v1 / putnam-1963-b6

putnam-1963-b6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1963-b6

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-1963-b6.lean

import Mathlib

open Topology Filter Polynomial

theorem putnam_1963_b6 (d : ℕ)
(S : Set (Fin d → ℝ) → Set (Fin d → ℝ))
(hS : S = fun A : Set (Fin d → ℝ) => ⋃ p ∈ A, ⋃ q ∈ A, segment ℝ p q)
(A : ℕ → Set (Fin d → ℝ))
(ddim : 1 ≤ d ∧ d ≤ 3)
(hA0 : Nonempty (A 0))
(hAn : ∀ n ≥ 1, A n = S (A (n - 1)))
: ∀ n ≥ 2, A n = A (n + 1) := by
  sorry

Runs (0)

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