Problem (2024KoMaLA878): Let point $A$ be one of the intersections of circles $c$ and $k$. Let $X_1$ and $X_2$ be arbitrary points on circle $c$. Let $Y_i$ denote the intersection of line $AX_i$ and circle $k$ for $i=1,2$. Let $P_1$, $P_2$ and $P_3$ be arbitrary points on circle $k$, and let $O$ denote the center of circle $k$. Let $K_{ij}$ denote the center of circle $(X_iY_iP_j)$ for $i=1,2$ and $j=1,2,3$. Let $L_j$ denote the center of circle $(OK_{1j}K_{2j})$ for $j=1,2,3$. Prove that points $L_1$, $L_2$ and $L_3$ are collinear.
AlphaGeometry formalization: a = free; oc = free; o = free; x1 = on_circle oc a; x2 = on_circle oc a; y1 = on_line a x1, on_circle o a; y2 = on_line a x2, on_circle o a; p1 = on_circle o a; p2 = on_circle o a; p3 = on_circle o a; k11 = circumcenter x1 y1 p1; k21 = circumcenter x2 y2 p1; k12 = circumcenter x1 y1 p2; k22 = circumcenter x2 y2 p2; k13 = circumcenter x1 y1 p3; k23 = circumcenter x2 y2 p3; l1 = circumcenter o k11 k21; l2 = circumcenter o k12 k22; l3 = circumcenter o k13 k23 ? coll l1 l2 l3
HAGeo formalization: A = point; Oc = point; O = point; (Oc) = circle_center_point Oc A; (O) = circle_center_point O A; A = intersection (Oc) (O); X1 = on_circle (Oc); X2 = on_circle (Oc); AX1 = line A X1; Y1 = intersection AX1 (O); AX2 = line A X2; Y2 = intersection AX2 (O); P1 = on_circle (O); P2 = on_circle (O); P3 = on_circle (O); K11 = circumcenter X1 Y1 P1; K12 = circumcenter X1 Y1 P2; K13 = circumcenter X1 Y1 P3; K21 = circumcenter X2 Y2 P1; K22 = circumcenter X2 Y2 P2; K23 = circumcenter X2 Y2 P3; L1 = circumcenter O K11 K21; L2 = circumcenter O K12 K22; L3 = circumcenter O K13 K23; Prove: collinear L1 L2 L3
Difficulty score: 3.7