Problem (2013CHNWesternMOp3): Let $ABC$ be a triangle, and $B_1,C_1$ be its excenters opposite $B,C$. $B_2,C_2$ are reflections of $B_1,C_1$ across midpoints of $AC,AB$. Let $D$ be the extouch at $BC$. Show that $AD$ is perpendicular to $B_2C_2$
AlphaGeometry formalization: a b c = triangle; b1 = excenter b c a; c1 = excenter c a b; m1 = midpoint a c; b2 = mirror b1 m1; m2 = midpoint a b; c2 = mirror c1 m2; a1 = excenter a b c; d = foot a1 b c ? perp a d b2 c2
HAGeo formalization: A B C = triangle; B1 = excenter B C A; C1 = excenter C A B; M = midpoint A C; N = midpoint A B; B2 = reflect B1 M; C2 = reflect C1 N; A1 = excenter A B C; BC = line B C; D = foot A1 BC; AD = line A D; B2C2 = line B2 C2; Prove: perpendicular AD B2C2
Difficulty score: 3.1