Problem (2014CTSTp13): Let the circumcenter of triangle $ABC$ be $O$. $H_A$ is the projection of $A$ onto $BC$. The extension of $AO$ intersects the circumcircle of $BOC$ at $A'$. The projections of $A'$ onto $AB, AC$ are $D,E$, and $O_A$ is the circumcentre of triangle $DH_AE$. Define $H_B, O_B, H_C, O_C$ similarly. Prove: $H_AO_A, H_BO_B, H_CO_C$ are concurrent
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h1 = foot a b c; h2 = foot b a c; h3 = foot c a b; o1 = circumcenter o b c; o2 = circumcenter o a c; o3 = circumcenter o b a; a1 = on_line a o, on_circle o1 o; b1 = on_line b o, on_circle o2 o; c1 = on_line c o, on_circle o3 o; d1 = foot a1 a b; d2 = foot a1 a c; u1 = circumcenter d1 h1 d2; e1 = foot b1 b c; e2 = foot b1 b a; u2 = circumcenter e1 h2 e2; f1 = foot c1 c a; f2 = foot c1 c b; u3 = circumcenter f1 h3 f2; t = on_line u1 h1, on_line u2 h2 ? coll t u3 h3
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; AC = line A C; AB = line A B; Ha = foot A BC; Hb = foot B AC; Hc = foot C AB; O1 = circumcenter O B C; O2 = circumcenter O A C; O3 = circumcenter O B A; AO = line A O; (BCO) = circle_center_point O1 O; BO = line B O; (ACO) = circle_center_point O2 O; CO = line C O; (ABO) = circle_center_point O3 O; A1 = intersection AO (BCO); B1 = intersection BO (ACO); C1 = intersection CO (ABO); D1 = foot A1 AB; D2 = foot A1 AC; Oa = circumcenter D1 Ha D2; E1 = foot B1 BC; E2 = foot B1 AB; Ob = circumcenter E1 Hb E2; F1 = foot C1 AC; F2 = foot C1 BC; Oc = circumcenter F1 Hc F2; HaOa = line Ha Oa; HbOb = line Hb Ob; T = intersection HaOa HbOb; Prove: collinear T Hc Oc
Difficulty score: 3.5