Problem (2005CMOp2): A circle meets the three sides $BC,CA,AB$ of a triangle $ABC$ at points $D_1,D_2;E_1,E_2; F_1,F_2$ respectively. Furthermore, line segments $D_1E_1$ and $D_2F_2$ intersect at point $L$, line segments $E_1F_1$ and $E_2D_2$ intersect at point $M$, line segments $F_1D_1$ and $F_2E_2$ intersect at point $N$. Prove that the lines $AL,BM,CN$ are concurrent.
AlphaGeometry formalization: a b c = triangle; o = free; d1 = on_line b c; d2 = on_line b c, on_circle o d1; e1 = on_line a c, on_circle o d1; e2 = on_line a c, on_circle o d1; f1 = on_line a b, on_circle o d1; f2 = on_line a b, on_circle o d1; l = on_line d1 e1, on_line d2 f2; m = on_line e1 f1, on_line e2 d2; n = on_line f1 d1, on_line f2 e2; p = on_line a l, on_line b m ? coll c n p
HAGeo formalization: A B C = triangle; O = point; BC = line B C; D1 = on_line BC; (O) = circle_center_point O D1; D2 = intersection (O) BC; AC = line A C; E1 E2 = intersection (O) AC; AB = line A B; F1 F2 = intersection (O) AB; D1E1 = line D1 E1; D2F2 = line D2 F2; L = intersection D1E1 D2F2; E1F1 = line E1 F1; D2E2 = line D2 E2; M = intersection E1F1 D2E2; D1F1 = line D1 F1; E2F2 = line E2 F2; N = intersection D1F1 E2F2; AL = line A L; BM = line B M; P = intersection AL BM; Prove: collinear C N P
Difficulty score: 2.3