# How to deduce circle theorems in Wolfram language?

I can deduce the first one by applying FindGeometricConjectures on the following scene:

GeometricScene[{
"A","B","C"
},{
Line[{{"A","B"},{"B","C"}}],CircleThrough[{"A","B","C"},Midpoint[{"A","C"}]]
}]


Next one:

GeometricScene[{
"A","B","C","D"
},{
Line[{{"A","B"},{"B","C"},{"A","D"},{"D","C"}}],CircleThrough[{"A","B","C","D"}]
}]


But the following is not working:

GeometricScene[{
"A","B","C","D"
},{
Line[{{"A","B"},{"B","C"},{"A","D"},{"D","C"}}],CircleThrough[{"A","B","C"},"D"]
}]

• With v12.1.1 on a Mac for the third example I get {EuclideanDistance["C", "D"] == EuclideanDistance["D", "A"]}. What result do you get that indicates that it is not working? Commented Sep 7, 2020 at 0:39
• @BobHanlon I also get the same on 12.1 but this is not the result I am after. This result is pretty obvious since CircleThrough[{"A","B","C"},"D"] means they are both radius. But the result I am after is PlanarAngle[{"A", "D", "C"}] == 2 PlanarAngle[{"A", "B", "C"}] Commented Sep 7, 2020 at 3:50
• Then I recommend that you edit your question to show what you tried, what you got, what you expected and why. Commented Sep 7, 2020 at 3:53

It seems that MMA can not find the general result but a special situation such as PlanarAngle equal to 30 Degree.
FindGeometricConjectures[