putnam-1969-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.

import Mathlib

open Matrix Filter Topology Set Nat
abbrev putnam_1969_b2_solution : Prop := False

theorem putnam_1969_b2 (P : ℕ → Prop)
    (P_def : ∀ n, P n ↔ ∀ (G : Type) [Group G] [Finite G],
      ∀ H : Fin n → Subgroup G, (∀ i, H i < ⊤) → ⋃ i, (H i : Set G) < ⊤) :
    P 2 ∧ (P 3 ↔ putnam_1969_b2_solution) := 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-1969-b2-s1

  open

  Open — not yet proved.

• putnam-1969-b2-s2

  open

  Open — not yet proved.

Runs (1)