putnam-v1 / putnam-1966-a2

putnam-1966-a2

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1966-a2

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-1966-a2.lean

import Mathlib

theorem putnam_1966_a2 (r : ℝ)
(A B C : EuclideanSpace ℝ (Fin 2))
(hABC : ¬Collinear ℝ {A, B, C})
(a b c p : ℝ)
(ha : a = dist B C)
(hb : b = dist C A)
(hc : c = dist A B)
(hp : p = (dist B C + dist C A + dist A B)/2)
(hr : ∃ I : EuclideanSpace ℝ (Fin 2),
(∃! P : EuclideanSpace ℝ (Fin 2), dist I P = r ∧ Collinear ℝ {P, B, C}) ∧
(∃! Q : EuclideanSpace ℝ (Fin 2), dist I Q = r ∧ Collinear ℝ {Q, C, A}) ∧
(∃! R : EuclideanSpace ℝ (Fin 2), dist I R = r ∧ Collinear ℝ {R, A, B}) ∧
(∀ Z : EuclideanSpace ℝ (Fin 2), dist I Z ≤ r → Z ∈ convexHull ℝ {A, B, C}))
: 1/(p - a)^2 + 1/(p - b)^2 + 1/(p - c)^2 ≥ 1/r^2 := by
  sorry

Runs (0)

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