Problem (2017CHNWesternMOp3): In triangle $ABC$, let $D$ be a point on $BC$. Let $I_1$ and $I_2$ be the incenters of triangles $ABD$ and $ACD$ respectively. Let $O_1$ and $O_2$ be the circumcenters of triangles $AI_1D$ and $AI_2D$ respectively. Let lines $I_1O_2$ and $I_2O_1$ meet at $P$. Show that $PD\perp BC$.
AlphaGeometry formalization: a b c = triangle; d = on_line b c; i1 = incenter a b d; i2 = incenter a c d; o1 = circumcenter a i1 d; o2 = circumcenter a i2 d; p = on_line i1 o2, on_line i2 o1 ? perp p d b c
HAGeo formalization: A B C = triangle; BC = line B C; D = on_line BC; I1 = incenter A B D; I2 = incenter A C D; O1 = circumcenter A I1 D; O2 = circumcenter A I2 D; I1O2 = line I1 O2; I2O1 = line I2 O1; P = intersection I1O2 I2O1; DP = line D P; Prove: perpendicular DP BC
Difficulty score: 4.2