Problem (2008CTSTp4): Let $ ABC$ be a triangle, line $ l$ cuts its sides $ BC,CA,AB$ at $ D,E,F$, respectively. Denote by $ O_{1},O_{2},O_{3}$ the circumcenters of triangle $ AEF,BFD,CDE$, respectively. Prove that the orthocenter of triangle $ O_{1}O_{2}O_{3}$ lies on line $ l$.
AlphaGeometry formalization: a b c = triangle; d = on_line b c; e = on_line a c; f = on_line a b, on_line d e; o1 = circumcenter a e f; o2 = circumcenter b f d; o3 = circumcenter c d e; h = orthocenter o1 o2 o3 ? coll d e h
HAGeo formalization: A B C = triangle; l = line; BC = line B C; D = intersection l BC; AC = line A C; E = intersection l AC; AB = line A B; F = intersection l AB; O1 = circumcenter A E F; O2 = circumcenter B F D; O3 = circumcenter C D E; H = orthocenter O1 O2 O3; Prove: collinear D E H
Difficulty score: 3.2