Problem (2015RMMp4): Let $ABC$ be a triangle, and let $D$ be the point where the incircle meets side $BC$. Let $J_b$ and $J_c$ be the incentres of the triangles $ABD$ and $ACD$, respectively. Prove that the circumcentre of the triangle $AJ_bJ_c$ lies on the angle bisector of $\angle BAC$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; j1 = incenter a b d; j2 = incenter a c d; o = circumcenter a j1 j2 ? eqangle b a a o a o a c
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; D = foot I BC; J1 = incenter A B D; J2 = incenter A C D; O = circumcenter A J1 J2; Prove: equal_angle B A O O A C
Difficulty score: 2.2