Problem (2010ARMOg11p3): Quadrilateral $ABCD$ is inscribed into circle $\omega$, $AC$ intersect $BD$ in point $K$. Points $M_1$, $M_2$, $M_3$, $M_4$-midpoints of arcs $AB$, $BC$, $CD$, and $DA$ respectively. Points $I_1$, $I_2$, $I_3$, $I_4$-incenters of triangles $ABK$, $BCK$, $CDK$, and $DAK$ respectively. Prove that lines $M_1I_1$, $M_2I_2$, $M_3I_3$, and $M_4I_4$ all intersect in one point.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; k = on_line a c, on_line b d; m1 = on_bline a b, on_circle o a; m2 = on_bline b c, on_circle o a; m3 = on_bline c d, on_circle o a; m4 = on_bline d a, on_circle o a; i1 = incenter a b k; i2 = incenter b c k; i3 = incenter c d k; i4 = incenter d a k; x = on_line m1 i1, on_line m2 i2 ? coll x m3 i3
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; AC = line A C; BD = line B D; K = intersection AC BD; M1 = midarc_no A B C; M2 = midarc_no B C D; M3 = midarc_no C D A; M4 = midarc_no D A B; I1 = incenter A B K; I2 = incenter B C K; I3 = incenter C D K; I4 = incenter D A K; I1M1 = line I1 M1; I2M2 = line I2 M2; X = intersection I1M1 I2M2; Prove: collinear X M3 I3
Difficulty score: 4.3