Problem (2019CTSTp1): $ABCDE$ is a cyclic pentagon, with circumcentre $O$. $AB=AE=CD$. $I$ midpoint of $BC$. $J$ midpoint of $DE$. $F$ is the orthocentre of $\triangle ABE$, and $G$ the centroid of $\triangle AIJ$.$CE$ intersects $BD$ at $H$, $OG$ intersects $FH$ at $M$. Show that $AM\perp CD$.
AlphaGeometry formalization: a b e = iso_triangle; o = circumcenter a b e; c = on_circle o a; d = on_circle o a, eqdistance d c b a; m = midpoint b c; n = midpoint d e; h = orthocenter a b e; g1 g2 g3 g = centroid a m n; p = on_line c e, on_line b d; t = on_line o g, on_line p h ? perp a t c d
HAGeo formalization: A B E = isos_triangle; O = circumcenter A B E; (O) = circle_center_point O A; C = on_circle (O); (C) = circle_center_radius C B A; D = intersection (O) (C); M = midpoint B C; N = midpoint D E; H = orthocenter A B E; G G1 G2 G3 = centroid A M N; CE = line C E; BD = line B D; P = intersection CE BD; OG = line O G; PH = line P H; T = intersection OG PH; AT = line A T; CD = line C D; Prove: perpendicular AT CD
Difficulty score: 4.6