Problem (2021CHNGaoLianA1): In triangle ABC,X,Y are on the angle bisector of ∠BAC and ∠ABX=∠ACY.BX intersects CY at P and circles (BYP) and (CXP) intersect at Q different from P. Prove that A,P,Q are on a line.
AlphaGeometry formalization: a b c = triangle; x = angle_bisector b a c; y = angle_bisector b a c, on_aline y c a a b x; p = on_line b x, on_line c y; o1 = circumcenter b y p; o2 = circumcenter c x p; q = on_circle o1 b, on_circle o2 c ? coll a p q
HAGeo formalization: A B C = triangle; l1 = angle_bisector B A C; X = on_line l1; l2 = angle_equal1 C A A B X; Y = intersection l1 l2; BX = line B X; CY = line C Y; P = intersection BX CY; O1 = circumcenter B Y P; (O1) = circle_center_point O1 B; O2 = circumcenter C X P; (O2) = circle_center_point O2 C; Q = intersection (O1) (O2); Prove: collinear A P Q
Difficulty score: 2.0