В честь позавчерашней статьи DeepMind об AlphaGeometry2 (обзор) вот те две геомы: 2018.6 и 2023.6, которые она не смогла решить. Красивые.

Делаем ставки: успеют ли люди записать решения все задач IMO в Lean вручную раньше, чем дипмайнды зарелизят AlphaProof и AlphaGeometry, которые сделают это автоматически.