Problem (2021IOMetrop2): Points $P$ and $Q$ are chosen on the side $BC$ of triangle $ABC$ so that $P$ lies between $B$ and $Q$. The rays $AP$ and $AQ$ divide the angle $BAC$ into three equal parts. It is known that the triangle $APQ$ is acute-angled. Denote by $B_1,P_1,Q_1,C_1$ the projections of points $B,P,Q,C$ onto the lines $AP,AQ,AP,AQ$, respectively. Prove that lines $B_1P_1$ and $C_1Q_1$ meet on line $BC$.
AlphaGeometry formalization: a b c = triangle; p q = trisect b a c; b1 = foot b a p; p1 = foot p a q; q1 = foot q a p; c1 = foot c a q; x = on_line b1 p1, on_line c1 q1 ? coll x b c
HAGeo formalization: A B C = triangle; l1 l2 = angle_trisector B A C; BC = line B C; P = intersection l1 BC; Q = intersection l2 BC; AP = line A P; B1 = foot B AP; AQ = line A Q; P1 = foot P AQ; Q1 = foot Q AP; C1 = foot C AQ; B1P1 = line B1 P1; C1Q1 = line C1 Q1; X = intersection B1P1 C1Q1; Prove: collinear X B C
Difficulty score: 1.6