Problem (2023SAGFp3): Let $P$ be a point on the bisector of $\angle BAC$. Line $BP,CP$ intersect $AC,AB$ at $E,D$, respectively. Tangents at $A$ WRT $\odot(ABC),\odot(ADE)$ intersect $BC,DE$ at $S,T$, respectively. $M$ is the Miquel point of $ADBPCE$ $(M = (CPE) \cap (BDP))$. Prove that $A,M,S,T$ are concyclic
AlphaGeometry formalization: a b c = triangle; p = angle_bisector b a c; e = on_line b p, on_line a c; d = on_line c p, on_line a b; o1 = circumcenter a b c; s = on_tline a o1 a, on_line b c; o2 = circumcenter a d e; t = on_tline a o2 a, on_line d e; o3 = circumcenter c p e; o4 = circumcenter b d p; m = on_circle o3 p, on_circle o4 p ? cyclic a m s t
HAGeo formalization: A B C = triangle; l = angle_bisector B A C; P = on_line l; BP = line B P; AC = line A C; E = intersection BP AC; CP = line C P; AB = line A B; D = intersection CP AB; O1 = circumcenter A B C; O1A = line O1 A; l1 = perpendicular_line A O1A; BC = line B C; S = intersection l1 BC; O2 = circumcenter A D E; O2A = line O2 A; l2 = perpendicular_line A O2A; DE = line D E; T = intersection l2 DE; O3 = circumcenter C P E; O4 = circumcenter B D P; (CEP) = circle_center_point O3 P; (BDP) = circle_center_point O4 P; M = intersection (CEP) (BDP); Prove: concyclic A M S T
Difficulty score: 4.8