Problem (ShuZhiMiGeo409): In acute $\triangle ABC$ with circumcenter $O$ and orthocenter $H$, line $OH$ meets $AB,AC$ at $X,Y$ with midpoint $T$. Draw $HE\parallel OB$ meeting $AC$ at $E$, and $HF\parallel OC$ meeting $AB$ at $F$. Let $D$ be $AH$'s midpoint and $EF$ meet $AT$ at $S$. Prove $S$ is the circumcenter of $\triangle OHD$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; x = on_line o h, on_line a b; y = on_line o h, on_line a c; t = midpoint x y; e = on_pline h o b, on_line a c; f = on_pline h o c, on_line a b; d = midpoint a h; s = on_line e f, on_line a t; s1 = on_tline o o d, on_tline h h d ? midp s d s1
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; OH = line O H; AB = line A B; X = intersection OH AB; AC = line A C; Y = intersection OH AC; T = midpoint X Y; OB = line O B; l1 = parallel_line H OB; E = intersection l1 AC; OC = line O C; l2 = parallel_line H OC; F = intersection l2 AB; D = midpoint A H; EF = line E F; AT = line A T; S = intersection EF AT; OD = line O D; l3 = perpendicular_line O OD; HD = line H D; l4 = perpendicular_line H HD; S1 = intersection l3 l4; Prove: midpoint S D S1
Difficulty score: 6.2