google-deepmind / google-deepmind/alphageometry
angle congruences, but not similarity
- 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
Assessment
This issue has not been assessed yet.