Problem (ShuZhiMiGeo209): In $\triangle ABC$ with angle bisectors $AD,BE,CF$ and altitudes $AX,BY,CZ$, let $P,Q,R$ be orthocenters of $\triangle AEF,\triangle BDF,\triangle CDE$, and $K,L,M$ be incenters of $\triangle AYZ,\triangle BZX,\triangle CXY$. Prove $PK,QL,MR$ concur on a common tangent to the incircle and nine-point circle.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = on_line b c, on_line a i; e = on_line c a, on_line b i; f = on_line a b, on_line c i; x = foot a b c; y = foot b c a; z = foot c a b; p = orthocenter a e f; q = orthocenter b f d; r = orthocenter c d e; k = incenter a y z; l = incenter b z x; m = incenter c x y; t = on_line p k, on_line q l; ni = circumcenter x y z; d1 = foot i b c; fe = on_circle i d1, on_circle ni x ? perp t fe i fe
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AI = line A I; D = intersection BC AI; CA = line C A; BI = line B I; E = intersection CA BI; AB = line A B; CI = line C I; F = intersection AB CI; X = foot A BC; Y = foot B CA; Z = foot C AB; P = orthocenter A E F; Q = orthocenter B F D; R = orthocenter C D E; K = incenter A Y Z; L = incenter B Z X; M = incenter C X Y; PK = line P K; QL = line Q L; T = intersection PK QL; Ni = circumcenter X Y Z; D1 = foot I BC; (I) = circle_center_point I D1; (Ni) = circle_center_point Ni X; Fe = intersection (I) (Ni); TFe = line T Fe; IFe = line I Fe; Prove: perpendicular TFe IFe
Difficulty score: 6.0