Problem (2011G6): Let $ABC$ be a triangle with $AB=AC$ and let $D$ be the midpoint of $AC$. The angle bisector of $\angle BAC$ intersects the circle through $D,B$ and $C$ at the point $E$ inside the triangle $ABC$. The line $BD$ intersects the circle through $A,E$ and $B$ in two points $B$ and $F$. The lines $AF$ and $BE$ meet at a point $I$, and the lines $CI$ and $BD$ meet at a point $K$. Show that $I$ is the incentre of triangle $KAB$.
AlphaGeometry formalization: a b c = iso_triangle; d = midpoint a c; o1 = circumcenter d b c; e = on_circle o1 d, angle_bisector b a c; o2 = circumcenter a e b; f = on_line b d, on_circle o2 a; i = on_line a f, on_line b e; k = on_line c i, on_line b d ? eqangle b a a i a i a k
HAGeo formalization: A B C = isos_triangle; D = midpoint A C; l1 = angle_bisector B A C; O1 = circumcenter D B C; (BCD) = circle_center_point O1 D; E = intersection l1 (BCD); BD = line B D; O2 = circumcenter A E B; (ABE) = circle_center_point O2 A; F = intersection BD (ABE); AF = line A F; BE = line B E; I = intersection AF BE; CI = line C I; K = intersection CI BD; Prove: equal_angle B A I I A K
Difficulty score: 3.2