4 ms·
I was all ready to be skeptical for most of these kind of works its outputs are 'not like human proofs' but then I saw Evan Chen's quote that it is indeed clean
by qrian 3y ago
I was all ready to be skeptical for most of these kind of works its outputs are 'not like human proofs' but then I saw Evan Chen's quote that it is indeed clean human-readable proof. Evan Chen is a prominent member of Olympiad math community and an author of famous Olympiad geometry book[1] so this time I will have to concede that machines indeed have conquered part of the IMO problems.
[1]: https://web.evanchen.cc/geombook.html https://web.evanchen.cc/geombook.html
- qrian 3y agoBut then again, there's an error in the proof of IMO P3, in Fig1.f and Step 26. of the full proof in supplimentary material[1], which it states that ∠GMD = ∠GO2D, which is incorrect. It should be ∠GMD + ∠GO2D = π. I am trying to follow its logic but I cannot parse Step 25. Did it hallucinate this step? It has the right idea of O2 being on the nine point circle though. edit: I retract my statement. It looks like it is using directed angles[2] which then the statement becomes correct. [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/alphageometry-an-olympiad-level-ai-system-for-geometry%20/AlphaGeometry%20solution.pdf https://storage.googleapis.com/deepmind-media/DeepMind.com/B... [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-Angles.pdf https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...
- polygamous_bat 3y agoI haven’t checked the proof yet, but could it be possible that it’s using directed angles? Threw me off initially when I first learned it as well, but it can be handy for different configurations.
- qrian 3y agoLooks like you are correct. I did not know about directed angles. Thanks.
- deleted 3y ago[deleted]