Problem (2017CTSTp9): Let $ABCD$ be a quadrilateral and let $l$ be a line. Let $l$ intersect the lines $AB,CD,BC,DA,AC,BD$ at points $X,X',Y,Y',Z,Z'$ respectively. Given that these six points on $l$ are in the order $X,Y,Z,X',Y',Z'$, show that the circles with diameter $XX',YY',ZZ'$ are coaxal.
AlphaGeometry formalization: a b c d = quadrangle; p1 p2 = segment; x = on_line p1 p2, on_line a b; x1 = on_line p1 p2, on_line c d; y = on_line p1 p2, on_line b c; y1 = on_line p1 p2, on_line d a; z = on_line p1 p2, on_line a c; z1 = on_line p1 p2, on_line b d; m1 = midpoint x x1; m2 = midpoint y y1; m3 = midpoint z z1; t = on_circle m1 x, on_circle m2 y ? perp t z t z1
HAGeo formalization: A B C D = quadrilateral; l = line; AB = line A B; X = intersection l AB; CD = line C D; X1 = intersection l CD; BC = line B C; Y = intersection l BC; AD = line A D; Y1 = intersection l AD; AC = line A C; Z = intersection l AC; BD = line B D; Z1 = intersection l BD; M1 = midpoint X X1; M2 = midpoint Y Y1; M3 = midpoint Z Z1; (M1) = circle_center_point M1 X; (M2) = circle_center_point M2 Y; T = intersection (M1) (M2); TZ = line T Z; TZ1 = line T Z1; Prove: perpendicular TZ TZ1
Difficulty score: 3.8