putnam-v1 / putnam-1963-a6

putnam-1963-a6

open

difficulty 4

credited

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

import Mathlib

open Topology Filter

theorem putnam_1963_a6 (F1 F2 U V A B C D P Q : EuclideanSpace ℝ (Fin 2))
(r : ℝ)
(E : Set (EuclideanSpace ℝ (Fin 2)))
(hE : E = {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r})
(M : EuclideanSpace ℝ (Fin 2))
(hMuv : M = midpoint ℝ U V)
(hr : r > dist F1 F2)
(hUV : U ∈ E ∧ V ∈ E ∧ U ≠ V)
(hAB : A ∈ E ∧ B ∈ E ∧ A ≠ B)
(hCD : C ∈ E ∧ D ∈ E ∧ C ≠ D)
(hAC : A ≠ C)
(hBD : B ≠ D)
(hdistinct : segment ℝ A B ≠ segment ℝ U V ∧ segment ℝ C D ≠ segment ℝ U V ∧ segment ℝ A B ≠ segment ℝ C D)
(hM : M ∈ segment ℝ A B ∧ M ∈ segment ℝ C D)
(hP : Collinear ℝ {P, A, C} ∧ Collinear ℝ {P, U, V})
(hQ : Collinear ℝ {Q, B, D} ∧ Collinear ℝ {Q, U, V})
: M = midpoint ℝ P Q := by
  sorry

Runs (0)

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