Problem (2021CzechAPSlovakp6): Let $ABC$ be an acute triangle and suppose points $A, A_b, B_a, B, B_c, C_b, C, C_a,$ and $A_c$ lie on its perimeter in this order. Let $A_1 \neq A$ be the second intersection point of the circumcircles of triangles $AA_bC_a$ and $AA_cB_a$. Analogously, $B_1 \neq B$ is the second intersection point of the circumcircles of triangles $BB_cA_b$ and $BB_aC_b$, and $C_1 \neq C$ is the second intersection point of the circumcircles of triangles $CC_aB_c$ and $CC_bA_c$. Suppose that the points $A_1, B_1,$ and $C_1$ are all distinct, lie inside the triangle $ABC$, and do not lie on a single line. Prove that lines $AA_1, BB_1, CC_1,$ and the circumcircle of triangle $A_1B_1C_1$ all pass through a common point.
AlphaGeometry formalization: a b c = triangle; a2 = on_line a b; b1 = on_line b a; b3 = on_line c b; c2 = on_line b c; c1 = on_line a c; a3 = on_line a c; o1 = circumcenter a a2 c1; o2 = circumcenter a a3 b1; a0 = on_circle o1 a, on_circle o2 a; o3 = circumcenter b b3 a2; o4 = circumcenter b b1 c2; b0 = on_circle o3 b, on_circle o4 b; o5 = circumcenter c c1 b3; o6 = circumcenter c c2 a3; c0 = on_circle o5 c, on_circle o6 c; x = on_line a a0, on_line b b0 ? cyclic x a0 b0 c0
HAGeo formalization: A B C = acute_triangle; AB = line A B; Ab = on_line AB; Ba = on_line AB; AC = line A C; Ac = on_line AC; Ca = on_line AC; BC = line B C; Bc = on_line BC; Cb = on_line BC; O1 = circumcenter A Ab Ca; (AAbCa) = circle_center_point O1 A; O2 = circumcenter A Ac Ba; (AAcBa) = circle_center_point O2 A; A1 = intersection (AAbCa) (AAcBa); O3 = circumcenter Ab B Bc; (AbBBc) = circle_center_point O3 B; O4 = circumcenter B Ba Cb; (BBaCb) = circle_center_point O4 B; B1 = intersection (AbBBc) (BBaCb); O5 = circumcenter Bc C Ca; (BcCCa) = circle_center_point O5 C; O6 = circumcenter Ac C Cb; (AcCCb) = circle_center_point O6 C; C1 = intersection (BcCCa) (AcCCb); AA1 = line A A1; BB1 = line B B1; X = intersection AA1 BB1; Prove: concyclic X A1 B1 C1
Difficulty score: 3.4