putnam-v1 / putnam-1967-b1

putnam-1967-b1

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1967-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.

goals/putnam-1967-b1.lean

import Mathlib

open Nat Topology Filter

theorem putnam_1967_b1 (r : ℝ)
(L : ZMod 6 → (EuclideanSpace ℝ (Fin 2)))
(P Q R: EuclideanSpace ℝ (Fin 2))
(hP : P = midpoint ℝ (L 1) (L 2))
(hQ : Q = midpoint ℝ (L 3) (L 4))
(hR : R = midpoint ℝ (L 5) (L 0))
(hr : r > 0)
(hcyclic : ∃ (O : EuclideanSpace ℝ (Fin 2)), ∀ i : ZMod 6, dist O (L i) = r)
(horder : ∀ i j : ZMod 6, i ≠ j → i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)
(hlens : dist (L 0) (L 1) = r ∧ dist (L 2) (L 3) = r ∧ dist (L 4) (L 5) = r)
(hdist : L 1 ≠ L 2 ∧ L 3 ≠ L 4 ∧ L 5 ≠ L 0)
: dist P Q = dist R P ∧ dist Q R = dist P Q := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.