Problem (2011AsiaPacificMOp3): Let $ABC$ be an acute triangle with $\angle BAC=30^{\circ}$. The internal and external angle bisectors of $\angle ABC$ meet the line $AC$ at $B_1$ and $B_2$, respectively, and the internal and external angle bisectors of $\angle ACB$ meet the line $AB$ at $C_1$ and $C_2$, respectively. Suppose that the circles with diameters $B_1B_2$ and $C_1C_2$ meet inside the triangle $ABC$ at point $P$. Prove that $\angle BPC=90^{\circ}$ .
AlphaGeometry formalization: o b c = ieq_triangle; a = on_circle o b; b1 = on_line a c, angle_bisector a b c; b2 = on_line a c, on_tline b b b1; c1 = on_line a b, angle_bisector a c b; c2 = on_line a b, on_tline c c c1; m1 = midpoint b1 b2; m2 = midpoint c1 c2; p = on_circle m1 b1, on_circle m2 c1 ? perp b p c p
HAGeo formalization: O B C = equilateral_triangle; (O) = circle_center_point O B; A = on_circle (O); l1 = angle_bisector A B C; AC = line A C; B1 = intersection l1 AC; l2 = angle_exbisector A B C; B2 = intersection l2 AC; l3 = angle_bisector A C B; AB = line A B; C1 = intersection l3 AB; l4 = angle_exbisector A C B; C2 = intersection l4 AB; M1 = midpoint B1 B2; (M1) = circle_center_point M1 B1; M2 = midpoint C1 C2; (M2) = circle_center_point M2 C1; P = intersection (M1) (M2); BP = line B P; CP = line C P; Prove: perpendicular BP CP
Difficulty score: 3.9