Problem (2019IranGOMp3): Three circles $\omega_1$, $\omega_2$ and $\omega_3$ pass through one common point, say $P$. The tangent line to $\omega_1$ at $P$ intersects $\omega_2$ and $\omega_3$ for the second time at points $P_{1,2}$ and $P_{1,3}$, respectively. Points $P_{2,1}$, $P_{2,3}$, $P_{3,1}$ and $P_{3,2}$ are similarly defined. Prove that the perpendicular bisector of segments $P_{1,2}P_{1,3}$, $P_{2,1}P_{2,3}$ and $P_{3,1}P_{3,2}$ are concurrent.
AlphaGeometry formalization: p = free; o1 = free; o2 = free; o3 = free; p12 = on_tline p o1 p, on_circle o2 p; p13 = on_tline p o1 p, on_circle o3 p; p21 = on_tline p o2 p, on_circle o1 p; p23 = on_tline p o2 p, on_circle o3 p; p31 = on_tline p o3 p, on_circle o1 p; p32 = on_tline p o3 p, on_circle o2 p; s = on_bline p12 p13, on_bline p21 p23 ? cong s p31 s p32
HAGeo formalization: P = point; O1 = point; O2 = point; O3 = point; (O1) = circle_center_point O1 P; (O2) = circle_center_point O2 P; (O3) = circle_center_point O3 P; PO1 = line P O1; PO2 = line P O2; PO3 = line P O3; l1 = perpendicular_line P PO1; l2 = perpendicular_line P PO2; l3 = perpendicular_line P PO3; P12 = intersection l1 (O2); P13 = intersection l1 (O3); P21 = intersection l2 (O1); P23 = intersection l2 (O3); P31 = intersection l3 (O1); P32 = intersection l3 (O2); m1 = perpendicular_bisector P12 P13; m2 = perpendicular_bisector P21 P23; S = intersection m1 m2; Prove: cong S P31 S P32
Difficulty score: 3.3