[qrian]

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

[qrian]

But 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/B...

[2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

[polygamous_bat]

I 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]

Looks like you are correct. I did not know about directed angles. Thanks.