Problem (2025KoeraFinalRoundp3): An acute triangle $\bigtriangleup ABC$ is given which $BC>CA>AB$. $I$ is the interior and the incircle of $\bigtriangleup ABC$ meets $BC, CA, AB$ at $D,E,F$. $AD$ and $BE$ meet at $P$. Let $l_{1}$ be a tangent from D to the circumcircle of $\bigtriangleup DIP$, and define $l_{2}$ and $l_{3}$ on $E$ and $F$, respectively. Prove $l_{1},l_{2},l_{3}$ meet at one point.
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; p = on_line a d, on_line b e; o1 = circumcenter d i p; o2 = circumcenter e i p; o3 = circumcenter f i p; q = on_tline d o1 d, on_tline e o2 e ? perp q f o3 f
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; D = foot I BC; E = foot I AC; F = foot I AB; AD = line A D; BE = line B E; P = intersection AD BE; O1 = circumcenter D I P; O2 = circumcenter E I P; O3 = circumcenter F I P; O1D = line O1 D; l1 = perpendicular_line D O1D; O2E = line O2 E; l2 = perpendicular_line E O2E; Q = intersection l1 l2; QF = line Q F; O3F = line O3 F; Prove: perpendicular QF O3F
Difficulty score: 5.8