Problem (2015USATSTp6): Let $ABC$ be a non-equilateral triangle and let $M_a$, $M_b$, $M_c$ be the midpoints of the sides $BC$, $CA$, $AB$, respectively. Let $S$ be a point lying on the Euler line. Denote by $X$, $Y$, $Z$ the second intersections of $M_aS$, $M_bS$, $M_cS$ with the nine-point circle. Prove that $AX$, $BY$, $CZ$ are concurrent.
AlphaGeometry formalization: a b c = triangle; ma = midpoint b c; mb = midpoint c a; mc = midpoint a b; o = circumcenter a b c; h = orthocenter a b c; s = on_line o h; n = circumcenter ma mb mc; x = on_line ma s, on_circle n ma; y = on_line mb s, on_circle n mb; z = on_line mc s, on_circle n mc; k = on_line a x, on_line b y ? coll k c z
HAGeo formalization: A B C = triangle; Ma = midpoint B C; Mb = midpoint C A; Mc = midpoint A B; Ni = circumcenter Ma Mb Mc; (Ni) = circle_center_point Ni Ma; O = circumcenter A B C; H = orthocenter A B C; OH = line O H; S = on_line O H; MaS = line Ma S; X = intersection MaS (Ni); MbS = line Mb S; Y = intersection MbS (Ni); McS = line Mc S; Z = intersection McS (Ni); AX = line A X; BY = line B Y; W = intersection AX BY; Prove: collinear W C Z
Difficulty score: 5.0