Problem (2022USATSTSTp6): Let $O$ and $H$ be the circumcenter and orthocenter, respectively, of an acute scalene triangle $ABC$. The perpendicular bisector of $\overline{AH}$ intersects $\overline{AB}$ and $\overline{AC}$ at $X_A$ and $Y_A$ respectively. Let $K_A$ denote the intersection of the circumcircles of triangles $OX_AY_A$ and $BOC$ other than $O$. Define $K_B$ and $K_C$ analogously by repeating this construction two more times. Prove that $K_A$, $K_B$, $K_C$, and $O$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; xa = on_bline a h, on_line a b; ya = on_bline a h, on_line a c; o_a = circumcenter o xa ya; o1 = circumcenter b o c; ka = on_circle o_a o, on_circle o1 o; xb = on_bline b h, on_line b c; yb = on_bline b h, on_line b a; o_b = circumcenter o xb yb; o2 = circumcenter a o c; kb = on_circle o_b o, on_circle o2 o; xc = on_bline c h, on_line c a; yc = on_bline c h, on_line c b; o_c = circumcenter o xc yc; o3 = circumcenter a o b; kc = on_circle o_c o, on_circle o3 o ? cyclic ka kb kc o
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; l1 = perpendicular_bisector A H; AB = line A B; Xa = intersection l1 AB; AC = line A C; Ya = intersection l1 AC; Oa = circumcenter O Xa Ya; (OXaYa) = circle_center_point Oa O; O1 = circumcenter B O C; (BCO) = circle_center_point O1 O; Ka = intersection (OXaYa) (BCO); l2 = perpendicular_bisector B H; BC = line B C; Xb = intersection l2 BC; Yb = intersection l2 AB; Ob = circumcenter O Xb Yb; (OXbYb) = circle_center_point Ob O; O2 = circumcenter A O C; (ACO) = circle_center_point O2 O; Kb = intersection (OXbYb) (ACO); l3 = perpendicular_bisector C H; Xc = intersection l3 AC; Yc = intersection l3 BC; Oc = circumcenter O Xc Yc; (OXcYc) = circle_center_point Oc O; O3 = circumcenter A O B; (ABO) = circle_center_point O3 O; Kc = intersection (OXcYc) (ABO); Prove: concyclic Ka Kb Kc O
Difficulty score: 4.5