Problem (2007USATSTp5): Triangle $ ABC$ is inscribed in circle $ \omega$. The tangent lines to $ \omega$ at $ B$ and $ C$ meet at $ T$. Point $ S$ lies on ray $ BC$ such that $ AS \perp AT$. Points $ B_1$ and $ C_1$ lie on ray $ ST$ (with $ C_1$ in between $ B_1$ and $ S$) such that $ B_1T = BT = C_1T$. Prove that triangles $ ABC$ and $ AB_1C_1$ are similar to each other.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; t = on_tline b o b, on_tline c o c; s = on_line b c, on_tline a a t; b1 = on_line s t, on_circle t b; c1 = on_line s t, on_circle t b ? simtri a b c a b1 c1
HAGeo formalization: A B C = triangle; O = circumcenter A B C; OB = line O B; OC = line O C; l1 = perpendicular_line B OB; l2 = perpendicular_line C OC; T = intersection l1 l2; AT = line A T; l3 = perpendicular_line A AT; BC = line B C; S = intersection BC l3; ST = line S T; (T) = circle_center_point T B; B1 C1 = intersection ST (T); Prove: similar A B C A B1 C1
Difficulty score: 3.2