Problem (2020USEMOp3): Let $ABC$ be an acute triangle with circumcenter $O$ and orthocenter $H$. Let $\Gamma$ denote the circumcircle of triangle $ABC$, and $N$ the midpoint of $OH$. The tangents to $\Gamma$ at $B$ and $C$, and the line through $H$ perpendicular to line $AN$, determine a triangle whose circumcircle we denote by $\omega_A$. Define $\omega_B$ and $\omega_C$ similarly. Prove that the common chords of $\omega_A$,$\omega_B$ and $\omega_C$ are concurrent on line $OH$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; n = midpoint o h; pa = on_tline b o b, on_tline c o c; qa = on_tline b o b, on_tline h a n; ra = on_tline c o c, on_tline h a n; o_a = circumcenter pa qa ra; pb = on_tline a o a, on_tline c o c; qb = on_tline a o a, on_tline h b n; rb = on_tline c o c, on_tline h b n; o_b = circumcenter pb qb rb; pc = on_tline a o a, on_tline b o b; qc = on_tline a o a, on_tline h c n; rc = on_tline b o b, on_tline h c n; o_c = circumcenter pc qc rc; k1 = on_circle o_a pa, on_circle o_b pb; k2 = on_circle o_a pa, on_circle o_b pb; j1 = on_circle o_b pb, on_circle o_c pc; j2 = on_circle o_b pb, on_circle o_c pc; t = on_line k1 k2, on_line j1 j2 ? coll t o h
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; N = midpoint O H; OA = line O A; OB = line O B; OC = line O C; la = perpendicular_line A OA; lb = perpendicular_line B OB; lc = perpendicular_line C OC; AN = line A N; ma = perpendicular_line H AN; BN = line B N; mb = perpendicular_line H BN; CN = line C N; mc = perpendicular_line H CN; Pa = intersection lb lc; Qa = intersection lb ma; Ra = intersection lc ma; Oa = circumcenter Pa Qa Ra; (Oa) = circle_center_point Oa Pa; Pb = intersection la mb; Qb = intersection la lc; Rb = intersection lc mb; Ob = circumcenter Pb Qb Rb; (Ob) = circle_center_point Ob Pb; Pc = intersection la mc; Qc = intersection lb mc; Rc = intersection la lb; Oc = circumcenter Pc Qc Rc; (Oc) = circle_center_point Oc Pc; U1 U2 = intersection (Oa) (Oc); V1 V2 = intersection (Ob) (Oc); U1U2 = line U1 U2; V1V2 = line V1 V2; X = intersection U1U2 V1V2; Prove: collinear X H O
Difficulty score: 5.9