Problem (2011ARMOg11p2): On side $BC$ of parallelogram $ABCD$ ($A$ is acute) lies point $T$ so that triangle $ATD$ is an acute triangle. Let $O_1$, $O_2$, and $O_3$ be the circumcenters of triangles $ABT$, $DAT$, and $CDT$ respectively. Prove that the orthocenter of triangle $O_1O_2O_3$ lies on line $AD$.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; t = on_line b c; o1 = circumcenter a b t; o2 = circumcenter d a t; o3 = circumcenter c d t; h = orthocenter o1 o2 o3 ? coll a d h
HAGeo formalization: A B C D = parallelogram; BC = line B C; T = on_line BC; O1 = circumcenter A B T; O2 = circumcenter D A T; O3 = circumcenter C D T; H = orthocenter O1 O2 O3; Prove: collinear A D H
Difficulty score: 3.2