Problem (1995USAMOp3): Given a nonisosceles, nonright triangle ABC, let O denote the center of its circumscribed circle, and let $A_1$, $B_1$, and $C_1$ be the midpoints of sides BC, CA, and AB, respectively. Point $A_2$ is located on the ray $OA_1$ so that $OAA_1$ is similar to $OA_2A$. Points $B_2$ and $C_2$ on rays $OB_1$ and $OC_1$, respectively, are defined similarly. Prove that lines $AA_2$, $BB_2$, and $CC_2$ are concurrent
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; a1 = midpoint b c; b1 = midpoint a c; c1 = midpoint a b; a2 = on_line o a1, on_aline a2 a o o a1 a; b2 = on_line o b1, on_aline b2 b o o b1 b; c2 = on_line o c1, on_aline c2 c o o c1 c; p = on_line a a2, on_line b b2 ? coll p c c2
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; A1 = midpoint B C; B1 = midpoint C A; C1 = midpoint A B; l1 = angle_equal1 A O O A1 A; OA1 = line O A1; A2 = intersection OA1 l1; l2 = angle_equal1 B O O B1 B; OB1 = line O B1; B2 = intersection OB1 l2; l3 = angle_equal1 C O O C1 C; OC1 = line O C1; C2 = intersection OC1 l3; AA2 = line A A2; BB2 = line B B2; P = intersection AA2 BB2; Prove: collinear P C C2
Difficulty score: 2.6