putnam-v1 / putnam-1964-a6

putnam-1964-a6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1964-a6

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-1964-a6.lean

import Mathlib

open Set Function Filter Topology

theorem putnam_1964_a6 (S : Finset ℝ)
(pairs : Set (ℝ × ℝ))
(hpairs : pairs = {(a, b) | (a ∈ S) ∧ (b ∈ S) ∧ (a < b)})
(distance : ℝ × ℝ → ℝ)
(hdistance : distance = fun (a, b) ↦ b - a)
(hrepdist : ∀ p ∈ pairs, (∃ m ∈ pairs, distance m > distance p) → ∃ q ∈ pairs, q ≠ p ∧ distance p = distance q)
: (∀ p q : pairs, q ≠ p → ∃ r : ℚ, distance p / distance q = r) := by
  sorry

Runs (0)

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