Problem (2018EuropeanMCupSp2): Let ABC be a triangle with$|AB|< |AC|. $ Let $k$ be the circumcircle of $\triangle ABC$ and let $O$ be the center of $k$. Point $M$ is the midpoint of the arc $BC $ of $k$ not containing $A$. Let $D $ be the second intersection of the perpendicular line from $M$ to $AB$ with $ k$ and $E$ be the second intersection of the perpendicular line from $M$ to $AC $ with $k$. Points $X $and $Y $ are the intersections of $CD$ and $BE$ with $OM$ respectively. Denote by $k_b$ and $k_c$ circumcircles of triangles $BDX$ and $CEY$ respectively. Let $G$ and $H$ be the second intersections of $k_b$ and $k_c $ with $AB$ and $AC$ respectively. Denote by ka the circumcircle of triangle $AGH.$ Prove that $O$ is the circumcenter of $\triangle O_aO_bO_c, $where $O_a, O_b, O_c $ are the centers of $k_a, k_b, k_c$ respectively.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = on_circle o a, angle_bisector b a c; d = on_circle o a, on_tline m a b; e = on_circle o a, on_tline m a c; x = on_line c d, on_line o m; y = on_line b e, on_line o m; o2 = circumcenter b d x; o3 = circumcenter c e y; g = on_line a b, on_circle o2 b; h = on_line a c, on_circle o3 c; o1 = circumcenter a g h ? cong o o1 o o2
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; M = midarc_no B C A; AB = line A B; l1 = perpendicular_line M AB; D = intersection l1 (O); AC = line A C; l2 = perpendicular_line M AC; E = intersection l2 (O); CD = line C D; MO = line M O; X = intersection CD MO; BE = line B E; Y = intersection BE MO; Ob = circumcenter B D X; (Ob) = circle_center_point Ob B; (CEY) = circumcircle C E Y; G = intersection (Ob) AB; H = intersection (CEY) AC; Oa = circumcenter A G H; Prove: cong O Oa O Ob
Difficulty score: 2.4