Problem (2021USEMOp3): Let $A_1C_2B_1A_2C_1B_2$ be an equilateral hexagon. Let $O_1$ and $H_1$ denote the circumcenter and orthocenter of $\triangle A_1B_1C_1$, and let $O_2$ and $H_2$ denote the circumcenter and orthocenter of $\triangle A_2B_2C_2$. Suppose that $O_1 \ne O_2$ and $H_1 \ne H_2$. Prove that the lines $O_1O_2$ and $H_1H_2$ are either parallel or coincide.
AlphaGeometry formalization: a1 b1 c1 = triangle; a2 = on_bline b1 c1; b2 = on_circle c1 a2, on_bline a1 c1; c2 = on_circle b1 a2, on_bline a1 b1; o1 = circumcenter a1 b1 c1; h1 = orthocenter a1 b1 c1; o2 = circumcenter a2 b2 c2; h2 = orthocenter a2 b2 c2 ? para o1 o2 h1 h2
HAGeo formalization: A1 B1 C1 = triangle; l1 = perpendicular_bisector B1 C1; A2 = on_line l1; l2 = perpendicular_bisector A1 C1; (C1) = circle_center_point C1 A2; B2 = intersection l2 (C1); l3 = perpendicular_bisector A1 B1; (B1) = circle_center_point B1 A2; C2 = intersection l3 (B1); O1 = circumcenter A1 B1 C1; H1 = orthocenter A1 B1 C1; O2 = circumcenter A2 B2 C2; H2 = orthocenter A2 B2 C2; O1O2 = line O1 O2; H1H2 = line H1 H2; Prove: parallel O1O2 H1H2
Difficulty score: 5.2