putnam-1966-a1

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

theorem putnam_1966_a1 (f : ℤ → ℤ)
(hf : f = fun n : ℤ => ∑ m ∈ Finset.Icc 0 n, (if Even m then m / 2 else (m - 1)/2))
: ∀ x y : ℤ, x > 0 ∧ y > 0 ∧ x > y → x * y = f (x + y) - f (x - y) := 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-a1-s1

  open

  Open — not yet proved.

• putnam-1966-a1-s2

  open

  Open — not yet proved.

• putnam-1966-a1-s3

  open

  Open — not yet proved.

Runs (1)