Problem (2005CTSTp1): Point $P$ lies inside triangle $ABC$. Let the projections of $P$ onto sides $BC$,$CA$,$AB$ be $D$, $E$, $F$ respectively. Let the projections from $A$ to the lines $BP$ and $CP$ be $M$ and $N$ respectively. Prove that $ME$, $NF$ and $BC$ are concurrent.
AlphaGeometry formalization: a b c = triangle; p = free; d = foot p b c; e = foot p a c; f = foot p a b; m = foot a b p; n = foot a c p; t = on_line m e, on_line b c ? coll t n f
HAGeo formalization: A B C = triangle; P = point; BC = line B C; D = foot P BC; AC = line A C; E = foot P AC; AB = line A B; F = foot P AB; BP = line B P; M = foot A BP; CP = line C P; N = foot A CP; EM = line E M; FN = line F N; T = intersection EM BC; Prove: collinear F N T
Difficulty score: 1.8