putnam-1966-b4

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_b4 (m n : ℕ)
(S : Finset ℕ)
(hS : (∀ i ∈ S, i > 0) ∧ S.card = m * n + 1)
: ∃ T ⊆ S, (T.card = m + 1 ∧ ∀ j ∈ T, ∀ i ∈ T, i ≠ j → ¬(j ∣ i)) ∨ (T.card = n + 1 ∧ ∀ i ∈ T, ∀ j ∈ T, j < i → j ∣ i) := 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-b4-s1

  open

  Open — not yet proved.

• putnam-1966-b4-s2

  open

  Open — not yet proved.

• putnam-1966-b4-s3

  open

  Open — not yet proved.

Runs (1)