Problem (2019IranGOMp4): Let $ABCD$ be a parallelogram and let $K$ be a point on line $AD$ such that $BK=AB$. Suppose that $P$ is an arbitrary point on $AB$, and the perpendicular bisector of $PC$ intersects the circumcircle of triangle $APD$ at points $X$, $Y$. Prove that the circumcircle of triangle $ABK$ passes through the orthocenter of triangle $AXY$.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; k = on_line a d, eqdistance k b a b; p = on_line a b; o1 = circumcenter a p d; x = on_bline p c, on_circle o1 a; y = on_bline p c, on_circle o1 a; h = orthocenter a x y ? cyclic a b k h
HAGeo formalization: A B C D = parallelogram; AD = line A D; (B) = circle_center_point B A; K = intersection AD (B); AB = line A B; P = on_line AB; l1 = perpendicular_bisector C P; O1 = circumcenter A D P; (ADP) = circle_center_point O1 A; X Y = intersection l1 (ADP); H = orthocenter A X Y; Prove: concyclic H A B K
Difficulty score: 3.7