google-deepmind / alphageometry

Apache License 2.0
4.1k stars 460 forks source link

Wrong Rule of Equal Inscribed Angle #97

Closed michael753-yen closed 5 months ago

michael753-yen commented 6 months ago

Here is the problem in nature language: There is a square ABCD with E as the intersection of its diagonals. F is a point on AD. Let G be a circle that passes through A, P, and F, intersects AC at Point H. translated into geometric language a b c d = isquare a b c d; p = on_line p a c, on_line p b d; e = on_line e a d; o = circle o a e p; f = on_circle f o a, on_line f a b ? cong d e a f 15603 alphageometry's proof is as following:

001. GA = GF [07] & GH = GA [10] & GF = GE [08] ⇒  A,H,E,F are concyclic [11]
002. A,H,E,F are concyclic [11] ⇒  ∠AHE = ∠AFE [12]
.....

Obviously, the 002 step is already wrong, it should be like ∠AHE+∠AFE=180° rather than ∠AHE = ∠AFE

I've tried to modify the rules.txt, but it doesn't work at all. Is there any way to fix it?

ghost commented 6 months ago

The program uses directional angles you can look that up on wikipedia

michael753-yen commented 6 months ago

It has nothing to do with directional angle. (here directional angle means 360°-∠AHE) ∠BHE = ∠AFE is right, but how can ∠AHE represents ∠BHE?

szhang99 commented 6 months ago

As Noxlgoldi said, this is correct, you can assume this one and follow all the logic, you will see it is correct.

michael753-yen commented 6 months ago

@szhang99 yeah, your're right. 003. A,D,F are collinear [06] & B,A,H are collinear [09] & ∠AHE = ∠AFE [12] ⇒ ∠DFE = ∠AHE [13] It got back on track immediately at the next step. So, maybe I'll just ignore it?

szhang99 commented 6 months ago

This is the correct syntax, treat two angles \alpha=\beta if and only if sin(\alpha)=sin(\beta), things always work(see Johnson's book Advanced Euclidean Geometry)

michael753-yen commented 5 months ago

@szhang99 thanks a lot! The book you mentioned is very helpful. Btw, I'm a Taiwanese student but I have never heard of "directed angle". Is it a common sense to you guys?