Problem (2021IsraelOlympicRev): Let $ABC$ be a triangle. A point $P$ is chosen inside $\triangle ABC$ such that $\angle BPC+\angle BAC=180^{\circ}$. The lines $AP,BP,CP$ intersect $BC,CA,AB$ at $P_A,P_B,P_C$ respectively. Let $X_A$ be the second intersection of the circumcircles of $\triangle ABC$ and $\triangle AP_BP_C$ . Similarly define $X_B,X_C$. Let $B'$ be the intersection of lines $AX_A,CX_C$, and let $C'$ be the intersection of lines $AX_A,BX_B$. Prove that lines $BB'$ and $CC'$ intersect on the circumcircle of $\triangle AP_BP_C$.
AlphaGeometry formalization: a b c = triangle; p = eqangle3 p b c a c b; p1 = on_line a p, on_line b c; p2 = on_line b p, on_line a c; p3 = on_line c p, on_line a b; o = circumcenter a b c; o2 = circumcenter a p2 p3; x1 = on_circle o a, on_circle o2 a; o3 = circumcenter b p3 p1; x2 = on_circle o b, on_circle o3 b; o4 = circumcenter c p1 p2; x3 = on_circle o c, on_circle o4 c; b1 = on_line a x1, on_line c x3; c1 = on_line a x1, on_line b x2; k = on_line b b1, on_line c c1 ? cyclic k a p2 p3
HAGeo formalization: A B C = triangle; ω1 = angle_equal2 B C C A B; P = on_circle ω1; AP = line A P; BC = line B C; P1 = intersection AP BC; BP = line B P; AC = line A C; P2 = intersection BP AC; CP = line C P; AB = line A B; P3 = intersection CP AB; O = circumcenter A B C; O2 = circumcenter A P2 P3; (O) = circle_center_point O A; (O2) = circle_center_point O2 A; X1 = intersection (O) (O2); O3 = circumcenter B P3 P1; (O3) = circle_center_point O3 B; X2 = intersection (O) (O3); O4 = circumcenter C P1 P2; (O4) = circle_center_point O4 C; X3 = intersection (O) (O4); AX1 = line A X1; CX3 = line C X3; B1 = intersection AX1 CX3; BX2 = line B X2; C1 = intersection AX1 BX2; BB1 = line B B1; CC1 = line C C1; K = intersection BB1 CC1; Prove: concyclic K A P2 P3
Difficulty score: 5.0