putnam-v1 / putnam-1965-a1

putnam-1965-a1

proved

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1965-a1

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-1965-a1.lean

import Mathlib

open EuclideanGeometry Real
noncomputable abbrev putnam_1965_a1_solution : ℝ := Real.pi / 15

theorem putnam_1965_a1 (A B C X Y : EuclideanSpace ℝ (Fin 2))
(hABC : ¬Collinear ℝ {A, B, C})
(hangles : ∠ C A B < ∠ B C A ∧ ∠ B C A < π/2 ∧ π/2 < ∠ A B C)
(hX : Collinear ℝ {X, B, C} ∧ ∠ X A B = (π - ∠ C A B)/2 ∧ dist A X = dist A B)
(hY : Collinear ℝ {Y, C, A} ∧ ∠ Y B C = (π - ∠ A B C)/2 ∧ dist B Y = dist A B)
: ∠ C A B = putnam_1965_a1_solution := by
  sorry

Runs (0)

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