Problem (2003USATSTp6): Let $\overline{AH_1}, \overline{BH_2}$, and $\overline{CH_3}$ be the altitudes of an acute scalene triangle $ABC$. The incircle of triangle $ABC$ is tangent to $\overline{BC}, \overline{CA},$ and $\overline{AB}$ at $T_1, T_2,$ and $T_3$, respectively. For $k = 1, 2, 3$, let $P_i$ be the point on line $H_iH_{i+1}$ (where $H_4 = H_1$) such that $H_iT_iP_i$ is an acute isosceles triangle with $H_iT_i = H_iP_i$. Prove that the circumcircles of triangles $T_1P_1T_2$, $T_2P_2T_3$, $T_3P_3T_1$ pass through a common point.
AlphaGeometry formalization: a b c = triangle; h1 = foot a b c; h2 = foot b a c; h3 = foot c a b; i = incenter a b c; t1 = foot i b c; t2 = foot i a c; t3 = foot i a b; p1 = on_line h1 h2, on_circle h1 t1; p2 = on_line h2 h3, on_circle h2 t2; p3 = on_line h3 h1, on_circle h3 t3; o1 = circumcenter t1 p1 t2; o2 = circumcenter t2 p2 t3; o3 = circumcenter t3 p3 t1; x = on_circle o1 t1, on_circle o2 t2 ? cong x o3 t3 o3
HAGeo formalization: A B C = acute_triangle; BC = line B C; H1 = foot A BC; AC = line A C; H2 = foot B AC; AB = line A B; H3 = foot C AB; I = incenter A B C; T1 = foot I BC; T2 = foot I AC; T3 = foot I AB; H1H2 = line H1 H2; (H1) = circle_center_point H1 T1; P1 = intersection H1H2 (H1); H2H3 = line H2 H3; (H2) = circle_center_point H2 T2; P2 = intersection H2H3 (H2); H1H3 = line H1 H3; (H3) = circle_center_point H3 T3; P3 = intersection H1H3 (H3); O1 = circumcenter T1 P1 T2; O2 = circumcenter T2 P2 T3; O3 = circumcenter T3 P3 T1; (O1) = circle_center_point O1 T1; (O2) = circle_center_point O2 T2; X = intersection (O1) (O2); Prove: cong X O3 T3 O3
Difficulty score: 3.0