Problem (2019KoMaLA754): Let $P$ be a point inside the acute triangle $ABC,$ and let $Q$ be the isogonal conjugate of $P.$ Let $L,M$ and $N$ be the midpoints of the shorter arcs $BC,CA$ and $AB$ of the circumcircle of $ABC,$ respectively. Let $X_A$ be the intersection of ray $LQ$ and circle $(PBC),$ let $X_B$ be the intersection of ray $MQ$ and circle $PCA,$ and let $X_C$ be the intersection of ray $NQ$ and circle $(PAB).$ Prove that $P,X_A,X_B$ and $X_C$ are concyclic or coincide.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = free; q = on_aline q a c b a p, on_aline q b a c b p; l = on_circle o a, angle_bisector b a c; m = on_circle o a, angle_bisector a b c; n = on_circle o a, angle_bisector b c a; o_a = circumcenter p b c; xa = on_line l q, on_circle o_a p; o_b = circumcenter p c a; xb = on_line m q, on_circle o_b p; o_c = circumcenter p a b; xc = on_line n q, on_circle o_c p ? cyclic p xa xb xc
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; P = point; l1 = angle_equal1 A C B A P; l2 = angle_equal1 B A C B P; Q = intersection l1 l2; L = midarc_no B C A; M = midarc_no C A B; N = midarc_no A B C; LQ = line L Q; Oa = circumcenter B C P; (BCP) = circle_center_point Oa P; Xa = intersection LQ (BCP); MQ = line M Q; Ob = circumcenter A C P; (ACP) = circle_center_point Ob P; Xb = intersection MQ (ACP); NQ = line N Q; Oc = circumcenter A B P; (ABP) = circle_center_point Oc P; Xc = intersection NQ (ABP); Prove: concyclic P Xa Xb Xc
Difficulty score: 3.8