putnam-v1 / putnam-1965-b2

putnam-1965-b2

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1965-b2

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-1965-b2.lean

import Mathlib

open EuclideanGeometry Topology Filter Complex

theorem putnam_1965_b2 (n : ℕ)
(hn : n > 1)
(won : Fin n → Fin n → Bool)
(hirrefl : ∀ i : Fin n, won i i = false)
(hantisymm : ∀ i j : Fin n, i ≠ j → won i j = ¬won j i)
(w l : Fin n → ℤ)
(hw : w = fun r : Fin n => ∑ j : Fin n, (if won r j then 1 else 0))
(hl : l = fun r : Fin n => n - 1 - w r)
: ∑ r : Fin n, (w r)^2 = ∑ r : Fin n, (l r)^2 := by
  sorry

Runs (0)

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