Problem (2020AQGOp3): Let $\triangle{ABC}$ be a triangle with circumcenter $O$. Let $M,N$ be the midpoints of $\overline{AB}$ and $\overline{AC}$ respectively and let $T$ be the projection of $O$ on $\overline{MN}$. Let $D$ be the projection of $A$ on $\overline{BC}$. Let $\overline{TD}$ intersect $\odot(BOC)$ at points $U$ and $V$. Let $\odot(AUV)$ intersct $\overline{MN}$ at points $X,Y$. Let $\overline{AY}$ intersect $\odot(AMN)$ at $R$ and $\overline{AX}$ intersect $\odot(AMN)$ at $S$. Then show that $\overline{AO},\overline{RS},\overline{MN}$ are concurrent.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = midpoint a b; n = midpoint a c; t = foot o m n; d = foot a b c; o1 = circumcenter b o c; u = on_line t d, on_circle o1 b; v = on_line t d, on_circle o1 b; o2 = circumcenter a u v; x = on_line m n, on_circle o2 a; y = on_line m n, on_circle o2 a; o3 = circumcenter a m n; r = on_line a y, on_circle o3 a; s = on_line a x, on_circle o3 a; z = on_line a o, on_line r s ? coll z m n
HAGeo formalization: A B C = triangle; O = circumcenter A B C; M = midpoint A B; N = midpoint A C; MN = line M N; T = foot O MN; BC = line B C; D = foot A BC; DT = line D T; O1 = circumcenter B O C; (BCO) = circle_center_point O1 B; U V = intersection DT (BCO); O2 = circumcenter A U V; (AUV) = circle_center_point O2 A; X Y = intersection (AUV) MN; AY = line A Y; O3 = circumcenter A M N; (AMN) = circle_center_point O3 A; R = intersection AY (AMN); AX = line A X; S = intersection AX (AMN); AO = line A O; RS = line R S; W = intersection AO RS; Prove: collinear W M N
Difficulty score: 5.7