Problem (2018CzechAPSlovakp2-): Let $ABC$ be an acute scalene triangle. Let $D$ and $E$ be points on the sides $AB$ and $AC$, respectively, such that $BD=CE$. Denote by $O_1$ and $O_2$ the circumcentres of the triangles $ABE$ and $ACD$, respectively. Prove that the circumcircles of the triangles $ABC, ADE$, and $AO_1O_2$ have a common point different from $A$.
AlphaGeometry formalization: a b c = triangle; d = on_line a b; e = on_line a c, eqdistance c b d; o1 = circumcenter a b e; o2 = circumcenter a c d; o = circumcenter a b c; o3 = circumcenter a d e; x = on_circle o a, on_circle o3 a; o4 = circumcenter a o1 o2 ? cong x o4 a o4
HAGeo formalization: A B C = acute_triangle; AB = line A B; D = on_line AB; AC = line A C; (C) = circle_center_radius C B D; E = intersection AC (C); O1 = circumcenter A B E; O2 = circumcenter A C D; O = circumcenter A B C; (O) = circle_center_point O A; O3 = circumcenter A D E; (O3) = circle_center_point O3 A; X = intersection (O) (O3); O4 = circumcenter A O1 O2; Prove: cong X O4 A O4
Difficulty score: 3.1