Problem (2024TurkeyTSTp5): In a scalene triangle $ABC$, $H$ is the orthocenter, and $G$ is the centroid. Let $A_b$ and $A_c$ be points on $AB$ and $AC$, respectively, such that $B$, $C$, $A_b$, $A_c$ are cyclic, and the points $A_b$, $A_c$, $H$ are collinear. $O_a$ is the circumcenter of the triangle $AA_bA_c$. $O_b$ and $O_c$ are defined similarly. Prove that the centroid of the triangle $O_aO_bO_c$ lies on the line $HG$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; m1 m2 m3 g = centroid a b c; ab = on_line a b, on_tline h o a; ac = on_line a c, on_tline h o a; oa = circumcenter a ab ac; bc = on_line b c, on_tline h o b; ba = on_line b a, on_tline h o b; ob = circumcenter b bc ba; ca = on_line c a, on_tline h o c; cb = on_line c b, on_tline h o c; oc = circumcenter c ca cb; n1 n2 n3 g1 = centroid oa ob oc ? coll g1 h g
HAGeo formalization: A B C = triangle; O = circumcenter A B C; H = orthocenter A B C; G M1 M2 M3 = centroid A B C; AB = line A B; BC = line B C; AC = line A C; OA = line O A; l1 = perpendicular_line H OA; Ab = intersection AB l1; Ac = intersection AC l1; Oa = circumcenter A Ab Ac; OB = line O B; l2 = perpendicular_line H OB; Bc = intersection BC l2; Ba = intersection AB l2; Ob = circumcenter B Bc Ba; OC = line O C; l3 = perpendicular_line H OC; Ca = intersection AC l3; CB = line C B; Cb = intersection BC l3; Oc = circumcenter C Ca Cb; G1 N1 N2 N3 = centroid Oa Ob Oc; Prove: collinear G1 H G
Difficulty score: 5.1