putnam-1966-b1

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

theorem putnam_1966_b1 (n : ℕ)
(hn : n ≥ 3)
(L : ZMod n → (EuclideanSpace ℝ (Fin 2)))
(hsq : ∀ i : ZMod n, L i 0 ∈ Set.Icc 0 1 ∧ L i 1 ∈ Set.Icc 0 1)
(hnoncol : ∀ i j k : ZMod n, i ≠ j ∧ j ≠ k ∧ k ≠ i → ¬Collinear ℝ {L i, L j, L k})
(hconvex : ∀ i : ZMod n, segment ℝ (L i) (L (i + 1)) ∩ interior (convexHull ℝ {L j | j : ZMod n}) = ∅)
: ∑ i : Fin n, (dist (L i) (L (i + 1)))^2 ≤ 4 := 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-b1-s1

  open

  Open — not yet proved.

• putnam-1966-b1-s2

  open

  Open — not yet proved.

• putnam-1966-b1-s3

  blocked

  Open — not yet proved.

• putnam-1966-b1-s4

  blocked

  Open — not yet proved.

Runs (1)