Possibly wrong rule in the solver ruleset

[geometer]

The sample solution generated for the orthocentre problem by alhpageometry looks like this:

* From theorem premises:
A B C D : Points
BD ⟂ AC [00]
CD ⟂ AB [01]

 * Auxiliary Constructions:
E : Points
C,A,E are collinear [02]
B,D,E are collinear [03]

 * Proof steps:
001. E,C,A are collinear [02] & B,E,D are collinear [03] & BD ⟂ AC [00] ⇒  ∠CED = ∠BEA [04]
002. E,C,A are collinear [02] & B,E,D are collinear [03] & BD ⟂ AC [00] ⇒  ∠DEA = ∠CEB [05]
003. BD ⟂ AC [00] & CD ⟂ AB [01] ⇒  ∠BAC = ∠CDB [06]
004. B,D,E are collinear [03] & E,A,C are collinear [02] & ∠CDB = ∠BAC [06] ⇒  ∠CDE = ∠BAE [07]
005. ∠CED = ∠BEA [04] & ∠CDE = ∠BAE [07] (Similar Triangles)⇒  CE:BE = DE:EA [08]
006. CE:BE = DE:EA [08] & ∠DEA = ∠CEB [05] (Similar Triangles)⇒  ∠DAE = ∠CBE [09]
007. CE:BE = DE:EA [08] & ∠DEA = ∠CEB [05] (Similar Triangles)⇒  ∠EDA = ∠ECB [10]
008. ∠DAE = ∠CBE [09] & C,A,E are collinear [02] & B,D,E are collinear [03] & ∠EDA = ∠ECB [10] ⇒  AD ⟂ BC
==========================

I0118 18:44:43.041623 139894856428416 alphageometry.py:575] Solved.

As far as I understand, step 003 is wrong: the statement is correct for the angles between two straight lines, not for angles BAC and CDB. Does that mean the network has generated the wrong text? Or it just used a rule from the set, and the rule is wrong?

[mirefek]

I think it is correct. In my view, the general rule would be that if there are 4 lines a, b, c, d, then a ⟂ b & c ⟂ d ⇒ ∠db =∠ca (oriented angles modulo pi). In this case, we instantiate a = BD, b = AC, c = CD, d = AB, and write angles just with three points with the main vertex in the middle, that is ∠db = ∠(AB)(AC) = ∠BAC, and ∠ca = ∠(CD)(BD) = ∠CDB

[sonnguyenasu]

I think it is indeed a wrong statement. If ABC is an acute triangle and D is the orthocenter of ABC (based on the premises). Then D lie inside the triangle and making BAC = 180 - CDB. Hope to see some response on this. My prediction is the language model might be off on this step.

[Jerry-Master]

Angles are full angles. BAC=180-CDB implies ∠CDB = ∠BAC as of the definition of angles in DD.

[xx205]

I think it is indeed a wrong statement. If ABC is an acute triangle and D is the orthocenter of ABC (based on the premises). Then D lie inside the triangle and making BAC = 180 - CDB. Hope to see some response on this. My prediction is the language model might be off on this step.

Also there are degenerate cases when ABC is a right triangle.

[geometer]

Angles are full angles. BAC=180-CDB implies ∠CDB = ∠BAC as of the definition of angles in DD.

Ok, that's a possible interpretation. (Is there a source where we can view the list of definitions of DD?)

But then the step 006 looks wrong. Full angles are not enough here.

[Jerry-Master]

http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf Contains a good explanation of many predicates. But some are new here.

Why does 006 looks wrong? If ratios are congruent and angles are congruent, then triangles are similar.

[geometer]

Why does 006 looks wrong? If ratios are congruent and angles are congruent, then triangles are similar.

Because the congruent angles are full angles, but for similarity we need the traditional interpretation of the angles congruency.

[Jerry-Master]

In this case it does not matter because the angle is 90º, so it is still valid. And in the last step, it is also needed to assume that the angle is 90º to arrive at the conclusion which is not stated. Maybe the traceback function did not work well and lost some steps in the process. But the proof seems valid. Further clarification from authors is needed to know if the failure is on the traceback or the deduction steps.

[thtrieu]

I think it is indeed a wrong statement. If ABC is an acute triangle and D is the orthocenter of ABC (based on the premises). Then D lie inside the triangle and making BAC = 180 - CDB.

We use oriented/directed/full angles, where both cases are covered.

Because the congruent angles are full angles, but for similarity we need the traditional interpretation of the angles congruency.

In this case it does not matter because the angle is 90º, so it is still valid.

Yes it is valid because of 90. For angles other than 90, you can confirm the step is valid with the diagram (https://github.com/google-deepmind/alphageometry/commit/82364a7f3f245ba00df5574a1db40bf38def9a7f).

And in the last step, it is also needed to assume that the angle is 90º to arrive at the conclusion which is not stated. Maybe the traceback function did not work well and lost some steps in the process. But the proof seems valid. Further clarification from authors is needed to know if the failure is on the traceback or the deduction steps.

There is no need for the angle to be 90, using the premises of [008]:

∠DAE = ∠CBE [09] ∠EDA = ∠ECB [10] => ∠AED = ∠BEC [008a]

∠AED = ∠BEC [008a] C,A,E are collinear [02] => ∠(AC, ED) = ∠(BE, AC) [008b]

∠(AC, ED) = ∠(BE, AC) [008b] B,D,E are collinear [03] => ∠(AC, ED) = ∠(ED, AC) [008c]

∠(AC, ED) = ∠(ED, AC) [008c] => AC ⟂ ED [*]

So the "angle = 90 [*]" that you need is already in the premise.

[geometer]

Because the congruent angles are full angles, but for similarity we need the traditional interpretation of the angles congruency.

In this case it does not matter because the angle is 90º, so it is still valid.

Yes it is valid because of 90. For angles other than 90, you can confirm the step is valid with the diagram (82364a7).

Sorry, I didn't understand. On step 006, the solver used the rule r39:

eqratio6 B A B C Q P Q R, eqangle6 B A B C Q P Q R, ncoll A B C => simtri* A B C P Q R

Could you please clarify, does eqangle6 mean the full angles congruency?

If yes, the rule looks wrong to me.

[sonnguyenasu]

I think there is an example where step 6 might be false if applied definition of directed angle: Consider a right triangle ABC with M be midpoint of BC. Then ∠CMA=∠AMB, and CM/AM=AM/BM (as MA=MB=MC). However, AMB and AMC are not similar, because the angles are not congruent. If the triangles are similar because the angles are 90 degree like in the case of the OP's problem, it should be stated out in the statement.

[tpgh24]

Angles in AlphaGeometry have direction (sign). I made some improvements in a fork repository and have some ideas to further improve the performance of AlphaGeometry, check out AG4Masses and issue 110. I also shared my experiences with AG, including explanation of the sign of angle issue.