Problem (2023IranGOAp5): In triangle $ABC$ points $M$ and $N$ are the midpoints of sides $AC$ and $AB$, respectively and $D$ is the projection of $A$ into $BC$. Point $O$ is the circumcenter of $ABC$ and circumcircles of $BOC$, $DMN$ intersect at points $R, T$. Lines $DT$, $DR$ intersect line $MN$ at $E$ and $F$, respectively. Lines $CT$, $BR$ intersect at $K$. A point $P$ lies on $KD$ such that $PK$ is the angle bisector of $\angle BPC$. Prove that the circumcircles of $ART$ and $PEF$ are tangent.
AlphaGeometry formalization: a b c = triangle; m = midpoint a c; n = midpoint a b; d = foot a b c; o = circumcenter a b c; r = on_circum b o c, on_circum d m n; t = on_circum b o c, on_circum d m n; e = on_line d t, on_line m n; f = on_line d r, on_line m n; k = on_line c t, on_line b r; x = on_bline b c, on_line k d; p = on_line k d, on_circum b c x; o3 = circumcenter a r t; o4 = circumcenter p e f; a1 = on_line o3 o4, on_circle o4 p ? midp o4 a a1
HAGeo formalization: A B C = triangle; M = midpoint A C; N = midpoint A B; BC = line B C; D = foot A BC; O = circumcenter A B C; (BOC) = circumcircle B O C; (DMN) = circumcircle D M N; R = intersection (BOC) (DMN); T = intersection (BOC) (DMN); DT = line D T; MN = line M N; E = intersection DT MN; DR = line D R; F = intersection DR MN; CT = line C T; BR = line B R; K = intersection CT BR; l1 = perpendicular_bisector B C; KD = line K D; X = intersection l1 KD; (BCX) = circumcircle B C X; P = intersection KD (BCX); O3 = circumcenter A R T; O4 = circumcenter P E F; O3O4 = line O3 O4; (O4) = circle_center_point O4 P; A1 = intersection O3O4 (O4); Prove: midpoint O4 A A1
Difficulty score: 6.3