Problem (2017G4): In triangle $ABC$, let $\omega$ be the excircle opposite to $A$. Let $D, E$ and $F$ be the points where $\omega$ is tangent to $BC, CA$, and $AB$, respectively. The circle $AEF$ intersects line $BC$ at $P$ and $Q$. Let $M$ be the midpoint of $AD$. Prove that the circle $MPQ$ is tangent to $\omega$.
AlphaGeometry formalization: a b c = triangle; i1 = excenter a b c; d = foot i1 b c; e = foot i1 a c; f = foot i1 a b; o1 = circumcenter a e f; p = on_line b c, on_circle o1 a; q = on_line b c, on_circle o1 a; m = midpoint a d; o2 = circumcenter m p q; u = on_circle o2 m, on_circle i1 d ? coll i1 u o2
HAGeo formalization: A B C = triangle; I1 = excenter A B C; BC = line B C; D = foot I1 BC; AC = line A C; E = foot I1 AC; AB = line A B; F = foot I1 AB; (I1) = circle_center_point I1 D; O1 = circumcenter A E F; (AEF) = circle_center_point O1 A; P = intersection BC (AEF); Q = intersection BC (AEF); M = midpoint A D; O2 = circumcenter M P Q; (MPQ) = circle_center_point O2 M; U = intersection (MPQ) (I1); Prove: collinear I1 U O2
Difficulty score: 3.2