Problem (2021ARMOg11p4): In triangle $ABC$ angle bisectors $AA_{1}$ and $CC_{1}$ intersect at $I$. Line through $B$ parallel to $AC$ intersects rays $AA_{1}$ and $CC_{1}$ at points $A_{2}$ and $C_{2}$ respectively. Let $O_{a}$ and $O_{c}$ be the circumcenters of triangles $AC_{1}C_{2}$ and $CA_{1}A_{2}$ respectively. Prove that $\angle{O_{a}BO_{c}} = \angle{AIC} $
AlphaGeometry formalization: a b c = triangle; a1 = on_line b c, angle_bisector b a c; c1 = on_line a b, angle_bisector a c b; i = incenter a b c; a2 = on_pline b a c, on_line a a1; c2 = on_pline b a c, on_line c c1; oa = circumcenter a c1 c2; oc = circumcenter c a1 a2 ? eqangle oa b b oc a i i c
HAGeo formalization: A B C = triangle; l1 = angle_bisector B A C; BC = line B C; A1 = intersection l1 BC; l2 = angle_bisector B C A; AB = line A B; C1 = intersection l2 AB; AA1 = line A A1; CC1 = line C C1; I = intersection AA1 CC1; AC = line A C; l3 = parallel_line B AC; A2 = intersection l3 AA1; l4 = parallel_line B AC; C2 = intersection l4 CC1; Oa = circumcenter A C1 C2; Oc = circumcenter C A1 A2; Prove: equal_angle Oa B Oc A I C
Difficulty score: 4.2