search

tpgh24 / ag4masses

Making Google Deepmind's AlphaGeometry accessible to the Masses
Apache License 2.0
34 stars 4 forks source link

Can I prove sth like AB=CD and AB=CD+EF? #8

Open thedeepdeepsky opened 4 months ago

thedeepdeepsky commented 4 months ago

Can I prove sth like AB=CD and AB=CD+EF?

tpgh24 commented 4 months ago

For AB=CD just write ? cong A B C D. AlphaGeometry does not support goals like AB=CD+EF, but you can add a point say G on line CD with DG=EF, then prove cong A B C G. You cannot specify on which side of point D G falls, so it can be either CD+EF or CD-EF, but you will find that for many problems, the conclusion does not depend on the side of the point, so both points actual work. Also, AlphaGeometry will try to not let points overlap, so if there is already a point H between C and D with HD=EF, then when you construct G, it will be on the other side of D