Problem (2025VietnamTSTp2): Let $ABC$ be an acute, non-isosceles triangle with orthocenter $H$. Let $D, E, F$ be the reflections of $H$ over $BC, CA, AB$, respectively, and let $A', B', C'$ be the reflections of $A, B, C$ over $BC, CA, AB$, respectively. Let $S$ be the circumcenter of triangle $A'B'C'$, and let $H'$ be the orthocenter of triangle $DEF$. Define $J$ as the center of the circle passing through the three projections of $H$ onto the lines $B'C', C'A', A'B'$. Prove that $HJ$ is parallel to $H'S$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; d = reflect h b c; e = reflect h c a; f = reflect h a b; a1 = reflect a b c; b1 = reflect b c a; c1 = reflect c a b; s = circumcenter a1 b1 c1; h1 = orthocenter d e f; p1 = foot h b1 c1; p2 = foot h c1 a1; p3 = foot h a1 b1; j = circumcenter p1 p2 p3 ? para h j h1 s
HAGeo formalization: A B C = triangle; H = orthocenter A B C; BC = line B C; AC = line A C; AB = line A B; D = reflect_point_wrt_line H BC; E = reflect_point_wrt_line H AC; F = reflect_point_wrt_line H AB; A1 = reflect_point_wrt_line A BC; B1 = reflect_point_wrt_line B AC; C1 = reflect_point_wrt_line C AB; S = circumcenter A1 B1 C1; H1 = orthocenter D E F; B1C1 = line B1 C1; C1A1 = line C1 A1; A1B1 = line A1 B1; P1 = foot H B1C1; P2 = foot H C1A1; P3 = foot H A1B1; J = circumcenter P1 P2 P3; HJ = line H J; H1S = line H1 S; Prove: parallel HJ H1S
Difficulty score: 6.6