Problem (2024ELMOSLp4): In quadrilateral $ABCD$ with incenter $I$, points $W,X,Y,Z$ lie on sides $AB, BC,CD,DA$ with $AZ=AW$, $BW=BX$, $CX=CY$, $DY=DZ$. Define $T=\overline{AC}\cap\overline{BD}$ and $L=\overline{WY}\cap\overline{XZ}$. Let points $O_a,O_b,O_c,O_d$ be such that $\angle O_aZA=\angle O_aWA=90^\circ$ (and cyclic variants), and $G=\overline{O_aO_c}\cap\overline{O_bO_d}$. Prove that $\overline{IL}\parallel\overline{TG}$.
AlphaGeometry formalization: t1 t2 t3 = triangle; i = circumcenter t1 t2 t3; t4 = on_circle i t1; a = on_tline t1 i t1, on_tline t2 i t2; b = on_tline t2 i t2, on_tline t3 i t3; c = on_tline t3 i t3, on_tline t4 i t4; d = on_tline t1 i t1, on_tline t4 i t4; w = on_line a b; x = on_line b c, on_circle b w; y = on_line c d, on_circle c x; z = on_line d a, on_circle d y; t = on_line a c, on_line b d; l = on_line w y, on_line x z; oa = on_tline z a z, on_tline w a w; ob = on_tline x b x, on_tline w b w; oc = on_tline y c y, on_tline x c x; od = on_tline z d z, on_tline y d y; g = on_line oa oc, on_line ob od ? para i l t g
HAGeo formalization: T1 T2 T3 = triangle; I = circumcenter T1 T2 T3; (I) = circle_center_point I T1; T4 = on_circle (I); IT1 = line I T1; IT2 = line I T2; IT3 = line I T3; IT4 = line I T4; l1 = perpendicular_line T1 IT1; l2 = perpendicular_line T2 IT2; A = intersection l1 l2; l3 = perpendicular_line T3 IT3; B = intersection l2 l3; l4 = perpendicular_line T4 IT4; C = intersection l3 l4; D = intersection l1 l4; AB = line A B; W = on_line AB; BC = line B C; (B,W) = circle_center_point B W; X = intersection BC (B,W); CD = line C D; (C,X) = circle_center_point C X; Y = intersection CD (C,X); AD = line A D; (D,Y) = circle_center_point D Y; Z = intersection AD (D,Y); AC = line A C; BD = line B D; T = intersection AC BD; WY = line W Y; XZ = line X Z; L = intersection WY XZ; l5 = perpendicular_line Z AD; l6 = perpendicular_line W AB; l7 = perpendicular_line X BC; l8 = perpendicular_line Y CD; Oa = intersection l5 l6; Ob = intersection l6 l7; Oc = intersection l7 l8; Od = intersection l5 l8; OaOc = line Oa Oc; ObOd = line Ob Od; G = intersection OaOc ObOd; IL = line I L; TG = line T G; Prove: parallel IL TG
Difficulty score: 5.1