google-deepmind / alphageometry

Apache License 2.0
4.1k stars 460 forks source link

error in algebraic reasoning #111

Open shenglih opened 5 months ago

shenglih commented 5 months ago

BA:AC = 1_/2 [00] & AC:BA = 2_/1 [01] (Ratio chase)⇒ AC = BA [25] which is flat-out wrong. this was one of the proof steps generated from running ddar on the problem


D E = square B C D E
F = on_dia F D A
G = on_line G B E
H = foot H A B C
I = excenter I A B D
J = psquare J E A
K = on_circum K F I E
L M = trisegment L M D B```

### with the question (proof target)

```? eqangle a b e h d h a c```
bughunter244 commented 5 months ago

It seems this is related to this issue: https://github.com/google-deepmind/alphageometry/issues/68

This codebase is really buggy and crashes all the time! There is this repo that claims to fix all the bugs. I'm trying to use it instead https://github.com/tpgh24/ag4masses

tpgh24 commented 4 months ago

@shenglih, can you post the entire problem? what you posted above seems to be missing a few lines in the beginning

tpgh24 commented 4 months ago

I figured it out, this is not the same bug as #68 but both are related to constant ratio problems. The bug is here, num, den should be flipped for cd_ab:

image

I created a fork AG4Masses that fixed many issues in AlphaGeometry, including this one and #68. Also added some additional features, documentation and idea on how to improve AG, check it out if you are interested.

I tested using a simple problem:

tt_rconst_bug
a b c = triangle12; d = midpoint a c ? cong a b a d

AlphaGeometry crashes on it. After these two fixes, AG4Masses handles it correctly.