Problem (2023MOSTMockp2): Let $\triangle A_1A_3A_5 \sim \triangle A_4A_6A_2$ with sides intersecting at $X_1,\dots,X_6$. For $1\leq i\leq6$, let $O_i$ be the circumcenter of $\triangle A_iX_iA_{i+1}$ ($A_7=A_1$). Prove $O_1O_4$, $O_2O_5$, $O_3O_6$ are concurrent.
AlphaGeometry formalization: a1 a3 a5 = triangle; a4 = free; a6 = free; a2 = on_aline a2 a4 a6 a5 a1 a3, on_aline a2 a6 a4 a5 a3 a1; x1 = on_line a1 a3, on_line a2 a6; x2 = on_line a1 a3, on_line a2 a4; x3 = on_line a2 a4, on_line a3 a5; x4 = on_line a3 a5, on_line a4 a6; x5 = on_line a1 a5, on_line a6 a4; x6 = on_line a1 a5, on_line a2 a6; o1 = circumcenter a1 x1 a2; o2 = circumcenter a2 x2 a3; o3 = circumcenter a3 x3 a4; o4 = circumcenter a4 x4 a5; o5 = circumcenter a5 x5 a6; o6 = circumcenter a6 x6 a1; k = on_line o1 o4, on_line o2 o5 ? coll k o3 o6
HAGeo formalization: A1 A3 A5 = triangle; A4 = point; A6 = point; l1 = angle_equal1 A4 A6 A5 A1 A3; l2 = angle_equal1 A6 A4 A5 A3 A1; A2 = intersection l1 l2; A1A3 = line A1 A3; A2A6 = line A2 A6; X1 = intersection A1A3 A2A6; A2A4 = line A2 A4; X2 = intersection A1A3 A2A4; A3A5 = line A3 A5; X3 = intersection A2A4 A3A5; A4A6 = line A4 A6; X4 = intersection A3A5 A4A6; A1A5 = line A1 A5; X5 = intersection A1A5 A4A6; X6 = intersection A1A5 A2A6; O1 = circumcenter A1 X1 A2; O2 = circumcenter A2 X2 A3; O3 = circumcenter A3 X3 A4; O4 = circumcenter A4 X4 A5; O5 = circumcenter A5 X5 A6; O6 = circumcenter A6 X6 A1; O1O4 = line O1 O4; O2O5 = line O2 O5; K = intersection O1O4 O2O5; Prove: collinear K O3 O6
Difficulty score: 5.2