Problem (2021GOWACAp4): Let $ABC$ be a triangle with incenter $I$. Let $l_A$ be the line through the midpoint of $\overline{BC}$ perpendicular to $\overline{AI}$. Define $l_B$ and $l_C$ similarly. Denote $\Theta$ to be the triangle formed by $l_A$, $l_B$, $l_C$, so that $\Theta$ has orthocenter $H$ and circumcircle $\Omega$. Show that the radical axis of $(ABC)$ and $\Omega$ bisects $\overline{IH}$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; m1 = midpoint b c; m2 = midpoint a c; m3 = midpoint a b; a1 = on_tline m2 b i, on_tline m3 c i; b1 = on_tline m1 a i, on_tline m3 c i; c1 = on_tline m1 a i, on_tline m2 b i; h = orthocenter a1 b1 c1; m = midpoint i h; o = circumcenter a b c; o1 = circumcenter a1 b1 c1; x = on_circle o a, on_circle o1 a1; y = on_circle o a, on_circle o1 a1 ? coll x y m
HAGeo formalization: A B C = triangle; I = incenter A B C; D = midpoint B C; AI = line A I; la = perpendicular_line D AI; E = midpoint A C; BI = line B I; lb = perpendicular_line E BI; F = midpoint A B; CI = line C I; lc = perpendicular_line F CI; X = intersection lb lc; Y = intersection la lc; Z = intersection la lb; H = orthocenter X Y Z; O1 = circumcenter X Y Z; (XYZ) = circle_center_point O1 X; O = circumcenter A B C; (ABC) = circle_center_point O A; U V = intersection (XYZ) (ABC); M = midpoint H I; Prove: collinear U V M
Difficulty score: 3.5