google-deepmind / google-deepmind/alphageometry

angle congruences, but not similarity

Open
#74 4 comments 0 reactions 0 assignees View on GitHub
Dominant language
Python
Stars
4.9k
Forks
572
PR merge metrics
No merged PRs in 30d

Description

Not the following three theorems have exactly the same hypotheses.
```
test1
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? eqangle g d g c h b h c
test2
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? eqangle b c b d c g c d
test3
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? simtri c g d b h c
```
AG is able to prove the first two, which establish that two of corresponding angles in cgb and bhc are congruent; but it is unable to prove the third, that the two triangles are similar.

Thinking that combining test1 and test2 to deduce test3 might require a little more computing space, I tried increasing the parameters
```
BATCH_SIZE=2
BEAM_SIZE=2
DEPTH=2
```
But that didn't work

Anyone have an idea what's going on here?

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.