Problem (ShuZhiMi2024SpFp19): In $\triangle ABC$ with altitudes $AD,BE,CF$, let $I_1,I_2,I_3$ be incenters of $\triangle AEF,\triangle BFD,\triangle CDE$. For $l_a$ as the external common tangent of $(I_2),(I_3)$ distinct from $BC$ (similarly $l_b,l_c$), prove $l_a,l_b,l_c$ and $OI$ concur.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; d = foot a b c; e = foot b a c; f = foot c a b; i1 = incenter a e f; i2 = incenter b f d; i3 = incenter c d e; d2 = foot i2 b c; d3 = foot i3 b c; e1 = foot i1 a c; e3 = foot i3 a c; p2 = reflect d2 i2 i3; p3 = reflect d3 i2 i3; q1 = reflect e1 i1 i3; q3 = reflect e3 i1 i3; x = on_line p3 p2, on_line q1 q3 ? coll x i o
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; AC = line A C; AB = line A B; I = incenter A B C; D = foot A BC; E = foot B AC; F = foot C AB; I1 = incenter A E F; I2 = incenter B F D; I3 = incenter C D E; D2 = foot I2 BC; D3 = foot I3 BC; E1 = foot I1 AC; E3 = foot I3 AC; I2I3 = line I2 I3; P2 = reflect_point_wrt_line D2 I2I3; P3 = reflect_point_wrt_line D3 I2I3; I1I3 = line I1 I3; Q1 = reflect_point_wrt_line E1 I1I3; Q3 = reflect_point_wrt_line E3 I1I3; P3P2 = line P3 P2; Q1Q3 = line Q1 Q3; X = intersection P3P2 Q1Q3; Prove: collinear X I O
Difficulty score: 5.1