Problem (2019RMMSLG1): Let $BM$ be a median in an acute-angled triangle $ABC$. A point $K$ is chosen on the line through $C$ tangent to the circumcircle of $\vartriangle BMC$ so that $\angle KBC = 90^\circ$. The segments $AK$ and $BM$ meet at $J$. Prove that the circumcenter of $\triangle BJK$ lies on the line $AC$.
AlphaGeometry formalization: a b c = triangle; m = midpoint a c; o = circumcenter b m c; k = on_tline c o c, on_tline b b c; j = on_line a k, on_line b m; o1 = circumcenter b j k ? coll a c o1
HAGeo formalization: A B C = acute_triangle; M = midpoint A C; O = circumcenter B M C; OC = line O C; t1 = perpendicular_line C OC; BC = line B C; l1 = perpendicular_line B BC; K = intersection l1 t1; AK = line A K; BM = line B M; J = intersection AK BM; O1 = circumcenter B J K; Prove: collinear A C O1
Difficulty score: 3.3