Problem (2024ELMOSLp1): In convex quadrilateral $ABCD$, let diagonals $\overline{AC}$ and $\overline{BD}$ intersect at $E$. Let the circumcircles of $ADE$ and $BCE$ intersect $\overline{AB}$ again at $P \neq A$ and $Q \neq B$, respectively. Let the circumcircle of $ACP$ intersect $\overline{AD}$ again at $R \neq A$, and let the circumcircle of $BDQ$ intersect $\overline{BC}$ again at $S \neq B$. Prove that $A$, $B$, $R$, and $S$ are concyclic.
AlphaGeometry formalization: a b c d = quadrangle; e = on_line a c, on_line b d; p = on_line a b, on_circum a d e; q = on_line a b, on_circum b c e; r = on_line a d, on_circum a c p; s = on_line b c, on_circum b d q ? cyclic a b r s
HAGeo formalization: A B C D = quadrilateral; AC = line A C; BD = line B D; E = intersection AC BD; AB = line A B; (ADE) = circle A D E; P = intersection AB (ADE); (BCE) = circle B C E; Q = intersection AB (BCE); AD = line A D; (ACP) = circle A C P; R = intersection AD (ACP); BC = line B C; (BDQ) = circle B D Q; S = intersection BC (BDQ); Prove: concyclic A B R S
Difficulty score: 3.0