putnam-v1 / putnam-1969-a2

putnam-1969-a2

open

difficulty 4

credited

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

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

import Mathlib

open Matrix Filter Topology Set Nat

theorem putnam_1969_a2 (D : (n : ℕ) → Matrix (Fin n) (Fin n) ℝ)
(hD : D = fun (n : ℕ) => λ (i : Fin n) (j : Fin n) => |(i : ℝ) - (j : ℝ)| )
: ∀ n, n ≥ 2 → (D n).det = (-1)^((n : ℤ)-1) * ((n : ℤ)-1) * 2^((n : ℤ)-2) := by
  sorry

Runs (0)

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