Problem (2015IranGOAp1): let $ w_1 $ and $ w_2 $ two circles such that $ w_1 \cap w_2 = \{ A , B \} $ let $ X $ a point on $ w_2 $ and $ Y $ on $ w_1 $ such that $ BY \bot BX $ suppose that $ O $ is the center of $ w_1 $ and $ X' = w_2 \cap OX $ now if $ K = w_2 \cap X'Y $ prove $ X $ is the midpoint of arc $ AK $
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; x = on_circle o2 a; y = on_circle o1 a, on_tline b x b; x1 = on_line o1 x, on_circle o2 a; k = on_line x1 y, on_circle o2 a ? cong a x k x
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O = on_line l; P = on_line l; (O) = circle_center_point O A; (P) = circle_center_point P A; X = on_circle (P); BX = line B X; l1 = perpendicular_line B BX; Y = intersection (O) l1; OX = line O X; X1 = intersection OX (P); X1Y = line X1 Y; K = intersection (P) X1Y; Prove: cong A X X K
Difficulty score: 2.1