Problem (2021GOWACAp6): In scalene triangle $ABC$, let $I$ be its incenter and $\omega$ be its incircle. Let $\omega$ touch sides $\overline{BC}$, $\overline{CA}$, $\overline{AB}$ at $D$, $E$, $F$, respectively, and let $\overline{DI}$ and $\overline{EF}$ meet at $K$. Point $P$ lies on $\omega$ so that $\overline{DP} \perp \overline{EF}$, and $\overline{AP}$ meets $\omega$ again at $Q$. Lines $\overline{BQ}$, $\overline{CQ}$ meet $\omega$ again at $B_1$, $C_1$, and $\overline{B_1C_1}$ cuts $\overline{BC}$ at $X$. Prove that the line through the midpoints of $\overline{BC}$ and $\overline{EF}$, the line through $I$ parallel to $\overline{BC}$, and $\overline{KX}$ are concurrent.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; k = on_line d i, on_line e f; p = on_circle i d, on_tline d e f; q = on_line a p, on_circle i d; b1 = on_line b q, on_circle i d; c1 = on_line c q, on_circle i d; x = on_line b1 c1, on_line b c; m1 = midpoint b c; m2 = midpoint e f; t = on_line m1 m2, on_pline i b c ? coll t k x
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = foot I BC; (I) = circle_center_point I D; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; DI = line D I; EF = line E F; K = intersection DI EF; l1 = perpendicular_line D EF; P = intersection l1 (I); AP = line A P; Q = intersection AP (I); BQ = line B Q; B1 = intersection BQ (I); CQ = line C Q; C1 = intersection CQ (I); B1C1 = line B1 C1; X = intersection B1C1 BC; M = midpoint B C; N = midpoint E F; MN = line M N; l2 = parallel_line I BC; W = intersection l2 MN; Prove: collinear W K X
Difficulty score: 5.3