Золото Міжнародної математичної олімпіади
Дві лабораторії незалежно набрали 35 балів із 42, розв'язавши п'ять задач із шести звичайною мовою — без формальних систем і без інструментів.
Чому це важливо
Рік тому для срібла потрібна була спеціалізована система з машинною перевіркою; тепер золото взяла модель загального призначення, що просто міркує текстом.
AlphaProof 2024 року перекладав задачу мовою Lean, де кожен крок перевіряє машина. Тут моделі писали доведення природною мовою, як людина, і оцінювало їх людське журі за тими самими правилами. Часу вони мали стільки ж, скільки учасники — чотири з половиною години. Шоста задача не далася жодній. Різниця в підході важлива: формальна перевірка давала гарантію правильності, звичайна мова її не дає, тож надійність тепер тримається на самій моделі.