Problem (2012RMMp2): Given a non-isosceles triangle $ABC$, let $D,E$, and $F$ denote the midpoints of the sides $BC,CA$, and $AB$ respectively. The circle $BCF$ and the line $BE$ meet again at $P$, and the circle $ABE$ and the line $AD$ meet again at $Q$. Finally, the lines $DP$ and $FQ$ meet at $R$. Prove that the centroid $G$ of the triangle $ABC$ lies on the circle $PQR$.
AlphaGeometry formalization: a b c = triangle; d e f g = centroid a b c; p = on_line b e, on_circum b c f; q = on_line a d, on_circum a b e; r = on_line d p, on_line f q ? cyclic g p q r
HAGeo formalization: A B C = triangle; G D E F = centroid A B C; (BCF) = circle B C F; BE = line B E; P = intersection (BCF) BE; (ABE) = circle A B E; AD = line A D; Q = intersection (ABE) AD; DP = line D P; FQ = line F Q; R = intersection DP FQ; Prove: concyclic G P Q R
Difficulty score: 3.6