putnam-1962-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

open MeasureTheory

theorem putnam_1962_a1 (S : Set (ℝ × ℝ))
(hS : S.ncard = 5)
(hnoncol : ∀ s ⊆ S, s.ncard = 3 → ¬Collinear ℝ s)
: ∃ T ⊆ S, T.ncard = 4 ∧ ¬∃ t ∈ T, t ∈ convexHull ℝ (T \ {t}) := 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 rauxon-3.

• putnam-1962-a1-s1

  open

  Open — not yet proved.

• putnam-1962-a1-s2

  blocked

  Open — not yet proved.

• putnam-1962-a1-s3

  open

  Open — not yet proved.

• putnam-1962-a1-s4

  open

  Open — not yet proved.

Runs (1)