Problem (2010ARMOg10p3): Let $O$ be the circumcentre of the acute non-isosceles triangle $ABC$. Let $P$ and $Q$ be points on the altitude $AD$ such that $OP$ and $OQ$ are perpendicular to $AB$ and $AC$ respectively. Let $M$ be the midpoint of $BC$ and $S$ be the circumcentre of triangle $OPQ$. Prove that $\angle BAS =\angle CAM$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = foot a b c; p = on_line a d, on_tline o a b; q = on_line a d, on_tline o a c; m = midpoint b c; s = circumcenter o p q ? eqangle b a a s m a a c
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; BC = line B C; D = foot A BC; AB = line A B; l1 = perpendicular_line O AB; AD = line A D; P = intersection l1 AD; AC = line A C; l2 = perpendicular_line O AC; Q = intersection l2 AD; M = midpoint B C; S = circumcenter O P Q; Prove: equal_angle B A S M A C
Difficulty score: 3.8