Problem (ShuZhiMiGeo381): For $\triangle ABC$ with circumcenter $O$ and symmedian point $K$, let $A',B',C'$ be reflections of $A,B,C$ over opposite sides. If $O'$ and $H'$ are the circumcenter and orthocenter of $\triangle A'B'C'$, prove $H'K$ bisects segment $OO'$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m1 m2 m3 g = centroid a b c; k = on_aline k a b c a g, on_aline k b a c b g; a1 = reflect a b c; b1 = reflect b c a; c1 = reflect c a b; o1 = circumcenter a1 b1 c1; h1 = orthocenter a1 b1 c1; m = midpoint o o1 ? coll h1 k m
HAGeo formalization: A B C = triangle; O = circumcenter A B C; G M1 M2 M3 = centroid A B C; l1 = angle_equal1 A B C A G; l2 = angle_equal1 B A C B G; K = intersection l1 l2; BC = line B C; A1 = reflect_point_wrt_line A BC; AC = line A C; B1 = reflect_point_wrt_line B AC; AB = line A B; C1 = reflect_point_wrt_line C AB; O1 = circumcenter A1 B1 C1; H1 = orthocenter A1 B1 C1; M = midpoint O O1; Prove: collinear H1 K M
Difficulty score: 6.5