Problem (2013ARMOg9p7): Squares $CAKL$ and $CBMN$ are constructed on the sides of acute-angled triangle $ABC$, outside of the triangle. Line $CN$ intersects line segment $AK$ at $X$, while line $CL$ intersects line segment $BM$ at $Y$. Point $P$, lying inside triangle $ABC$, is an intersection of the circumcircles of triangles $KXN$ and $LYM$. Point $S$ is the midpoint of $AB$. Prove that angle $\angle ACS=\angle BCP$.
AlphaGeometry formalization: a b c = triangle; l k = square a c l k; m n = square c b m n; x = on_line c n, on_line a k; y = on_line c l, on_line b m; o1 = circumcenter k x n; o2 = circumcenter l y m; p = on_circle o1 k, on_circle o2 l; s = midpoint a b ? eqangle a c c s p c b c
HAGeo formalization: A B C = acute_triangle; L K = square A C; M N = square C B; CN = line C N; AK = line A K; X = intersection CN AK; CL = line C L; BM = line B M; Y = intersection CL BM; O1 = circumcenter K N X; (O1) = circle_center_point O1 K; O2 = circumcenter L M Y; (O2) = circle_center_point O2 L; P = intersection (O1) (O2); S = midpoint A B; Prove: equal_angle A C S P C B
Difficulty score: 2.8