Problem (2016USAMOp3): Let $\triangle ABC$ be an acute triangle, and let $I_B, I_C,$ and $O$ denote its $B$-excenter, $C$-excenter, and circumcenter, respectively. Points $E$ and $Y$ are selected on $\overline{AC}$ such that $\angle ABY=\angle CBY$ and $\overline{BE}\perp\overline{AC}$. Similarly, points $F$ and $Z$ are selected on $\overline{AB}$ such that $\angle ACZ=\angle BCZ$ and $\overline{CF}\perp\overline{AB}$. Lines $\overleftrightarrow{I_BF}$ and $\overleftrightarrow{I_CE}$ meet at $P$. Prove that $\overline{PO}$ and $\overline{YZ}$ are perpendicular.
AlphaGeometry formalization: a b c = triangle; ib = excenter b c a; ic = excenter c a b; o = circumcenter a b c; e = foot b a c; y = on_line a c, angle_bisector a b c; f = foot c a b; z = on_line a b, angle_bisector a c b; p = on_line ib f, on_line ic e ? perp p o y z
HAGeo formalization: A B C = acute_triangle; Ib = excenter B C A; Ic = excenter C A B; O = circumcenter A B C; l1 = angle_bisector A B C; AC = line A C; Y = intersection AC l1; l2 = angle_bisector A C B; AB = line A B; Z = intersection AB l2; E = foot B AC; F = foot C AB; FIb = line F Ib; EIc = line E Ic; P = intersection FIb EIc; OP = line O P; YZ = line Y Z; Prove: perpendicular OP YZ
Difficulty score: 4.0