putnam-v1 / putnam-1962-a3
putnam-1962-a3
open
difficulty 4
credited
Run this goal:
./swarm/run.sh --goal putnam-1962-a3What 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-1962-a3.lean
import Mathlib
open MeasureTheory
theorem putnam_1962_a3 (A B C A' B' C' P Q R : EuclideanSpace ℝ (Fin 2))
(k : ℝ)
(hk : k > 0)
(hABC : ¬Collinear ℝ {A, B, C})
(hA' : A' ∈ segment ℝ B C ∧ dist C A' / dist A' B = k)
(hB' : B' ∈ segment ℝ C A ∧ dist A B' / dist B' C = k)
(hC' : C' ∈ segment ℝ A B ∧ dist B C' / dist C' A = k)
(hP : P ∈ segment ℝ B B' ∧ P ∈ segment ℝ C C')
(hQ : Q ∈ segment ℝ C C' ∧ Q ∈ segment ℝ A A')
(hR : R ∈ segment ℝ A A' ∧ R ∈ segment ℝ B B')
: (volume (convexHull ℝ {P, Q, R})).toReal / (volume (convexHull ℝ {A, B, C})).toReal = (k - 1)^2 / (k^2 + k + 1) := by
sorry