Problem (2015CTSTp9): Let $ \triangle ABC $ be an acute triangle with circumcenter $ O $ and centroid $ G .$ Let $ D $ be the midpoint of $ BC $ and $ E\in \odot (BC) $ be a point inside $ \triangle ABC $ such that $ AE \perp BC  . $ Let $ F=EG \cap OD $ and $ K, L $ be the point lie on $ BC $ such that $ FK \parallel OB, FL \parallel OC . $ Let $ M \in AB $ be a point such that $ MK \perp BC $ and $ N \in AC $ be a point such that $ NL \perp BC . $ Let $ \omega $ be a circle tangent to $ OB, OC $ at $ B, C, $ respectively $ . $ Prove that $ \odot (AMN) $ is tangent to $ \omega $
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d d1 d2 g = centroid a b c; e = on_circle d b, on_tline a b c; f = on_line e g, on_line o d; k = on_line b c, on_pline f o b; l = on_line b c, on_pline f o c; m = on_line a b, on_tline k b c; n = on_line a c, on_tline l b c; o1 = on_bline b c, on_tline b o b; o2 = circumcenter a m n; t = on_circle o1 b, on_circle o2 a ? coll o2 o1 t
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; G D D1 D2 = centroid A B C; BC = line B C; l1 = perpendicular_line A BC; (BC) = circle_center_point D B; E = intersection (BC) l1; EG = line E G; DO = line D O; F = intersection EG DO; BO = line B O; l2 = parallel_line F BO; K = intersection BC l2; CO = line C O; l3 = parallel_line F CO; L = intersection BC l3; l4 = perpendicular_line K BC; AB = line A B; M = intersection AB l4; l5 = perpendicular_line L BC; AC = line A C; N = intersection AC l5; l6 = perpendicular_line B BO; l7 = perpendicular_line C CO; X = intersection l6 l7; (X) = circle_center_point X B; O2 = circumcenter A M N; (AMN) = circle_center_point O2 A; T = intersection (X) (AMN); Prove: collinear O2 X T
Difficulty score: 4.4