Problem (2023EuropeanMCupSp2): Let $ABC$ be a triangle such that $\angle BAC = 90^{\circ}$. The incircle of triangle $ABC$ is tangent to the sides $\overline{BC}$, $\overline{CA}$, $\overline{AB}$ at $D,E,F$ respectively. Let $M$ be the midpoint of $\overline{EF}$. Let $P$ be the projection of $A$ onto $BC$ and let $K$ be the intersection of $MP$ and $AD$. Prove that the circumcircles of triangles $AFE$ and $PDK$ have equal radius.
AlphaGeometry formalization: a b c = r_triangle; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; m = midpoint e f; p = foot a b c; k = on_line m p, on_line a d; o2 = circumcenter p d k ? cong m a o2 p
HAGeo formalization: A B C = right_triangle; I = incenter A B C; BC = line B C; D = foot I BC; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; M = midpoint E F; P = foot A BC; MP = line M P; AD = line A D; K = intersection MP AD; O2 = circumcenter P D K; Prove: cong A M O2 P
Difficulty score: 3.4