putnam-1967-a5

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 Nat Topology Filter

theorem putnam_1967_a5 (R : Set (EuclideanSpace ℝ (Fin 2)))
(hR : Convex ℝ R ∧ (MeasureTheory.volume R).toReal > Real.pi / 4)
: ∃ P ∈ R, ∃ Q ∈ R, dist P Q = 1 := 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-1967-a5-s1

  open

  Open — not yet proved.

• putnam-1967-a5-s2

  open

  Open — not yet proved.

• putnam-1967-a5-s3

  open

  Open — not yet proved.

• putnam-1967-a5-s4

  open

  Open — not yet proved.

Runs (1)