Problem (2015IranGOAp5): we have a triangle $ ABC $ and make rectangles $ ABA_1B_2 $ , $ BCB_1C_2 $ and $ CAC_1A_2 $ out of it. then pass a line through $ A_2 $ perpendicular to $ C_1A_2 $ and pass another line through $ A_1 $ perpendicular to $  A_1B_2 $. let $ A' $ the common point of this two lines. like this we make $ B' $ and $ C' $. prove $ AA' $ , $ BB' $ and $ CC' $ intersect each other in a same point.
AlphaGeometry formalization: a b c = triangle; a1 = on_tline b a b; b2 = parallelogram a b a1 b2; c2 = on_tline b c b; b1 = parallelogram c b c2 b1; a2 = on_tline c a c; c1 = parallelogram a c a2 c1; a3 = on_tline c2 a1 c2, on_tline b1 a2 b1; b3 = on_tline a2 b1 a2, on_tline c1 b2 c1; c3 = on_tline b2 c1 b2, on_tline a1 a1 c2; x = on_line a a3, on_line b b3 ? coll x c c3
HAGeo formalization: A B C = triangle; AB = line A B; t1 = perpendicular_line B AB; A1 = on_line t1; B2 = parallelogram A B A1; BC = line B C; t2 = perpendicular_line B BC; C2 = on_line t2; B1 = parallelogram C B C2; AC = line A C; t3 = perpendicular_line C AC; A2 = on_line t3; C1 = parallelogram A C A2; A1C2 = line A1 C2; l1 = perpendicular_line C2 A1C2; A2B1 = line A2 B1; l2 = perpendicular_line B1 A2B1; A3 = intersection l1 l2; l3 = perpendicular_line A2 A2B1; B2C1 = line B2 C1; l4 = perpendicular_line C1 B2C1; B3 = intersection l3 l4; l5 = perpendicular_line B2 B2C1; l6 = perpendicular_line A1 A1C2; C3 = intersection l5 l6; AA3 = line A A3; BB3 = line B B3; X = intersection AA3 BB3; Prove: collinear X C C3
Difficulty score: 4.5