Problem (ShuZhiMiGeo178): In $\triangle ABC$ with orthocenter $H$ and nine-point center $V$, let $\odot(AVH)\cap\odot(BVC)=X$ (similarly define $Y,Z$). Prove $AX,BY,CZ$ are concurrent.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; m1 = midpoint b c; m2 = midpoint c a; m3 = midpoint a b; v = circumcenter m1 m2 m3; o1 = circumcenter a v h; o2 = circumcenter b v c; x = on_circle o1 a, on_circle o2 b; o3 = circumcenter b v h; o4 = circumcenter c v a; y = on_circle o3 b, on_circle o4 c; o5 = circumcenter c v h; o6 = circumcenter a v b; z = on_circle o5 c, on_circle o6 a; k = on_line a x, on_line b y ? coll k c z
HAGeo formalization: A B C = triangle; H = orthocenter A B C; M1 = midpoint B C; M2 = midpoint C A; M3 = midpoint A B; V = circumcenter M1 M2 M3; O1 = circumcenter A V H; O2 = circumcenter B V C; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 B; X = intersection (O1) (O2); O3 = circumcenter B V H; O4 = circumcenter C V A; (O3) = circle_center_point O3 B; (O4) = circle_center_point O4 C; Y = intersection (O3) (O4); O5 = circumcenter C V H; O6 = circumcenter A V B; (O5) = circle_center_point O5 C; (O6) = circle_center_point O6 A; Z = intersection (O5) (O6); AX = line A X; BY = line B Y; K = intersection AX BY; Prove: collinear K C Z
Difficulty score: 6.1