Problem (2012G8): Let $ABC$ be a triangle with circumcircle $\omega$ and $\ell$ a line without common points with $\omega$. Denote by $P$ the foot of the perpendicular from the center of $\omega$ to $\ell$. The side-lines $BC,CA,AB$ intersect $\ell$ at the points $X,Y,Z$ different from $P$. Prove that the circumcircles of the triangles $AXP$, $BYP$ and $CZP$ have a common point different from $P$ or are mutually tangent at $P$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = free; p1 = on_tline p o p; x = on_line b c, on_line p p1; y = on_line c a, on_line p p1; z = on_line a b, on_line p p1; o1 = circumcenter a x p; o2 = circumcenter b y p; o3 = circumcenter c z p ? coll o1 o2 o3
HAGeo formalization: A B C = triangle; O = circumcenter A B C; l = line; P = foot O l; BC = line B C; X = intersection BC l; AC = line A C; Y = intersection AC l; AB = line A B; Z = intersection AB l; O1 = circumcenter A P X; O2 = circumcenter B P Y; O3 = circumcenter C P Z; Prove: collinear O1 O2 O3
Difficulty score: 4.9