OpenAI решила десять открытых математических задач. Настоящая новость — не решения, а то, где именно нашлись ошибки

OpenAI объявила о решении десяти сложных открытых математических задач с Lean-сертификатами, вместе с этим бенчмарком отметился и Бен Голуб. Впечатляющая работа, признаю без иронии — не так часто мне выпадает шанс это сказать про анонс из этой индустрии.

Но интересна мне не сама десятка решений, а стандарт верификации под ними. Ноль заглушек 'sorry' — специального маркера в Lean, которым помечают недоказанный шаг, — по всем десяти формализованным доказательствам. Это значит каждый логический шаг машинно проверен, а не просто заявлен на словах. Для тех, кто не в теме формальной верификации: это разница между 'мы посчитали и получилось' и 'компьютер независимо подтвердил каждую строчку рассуждения'.

При этом RefineDotInk нашёл несколько неточностей в самом описании работы — не в Lean-сертификатах, а именно в прозе, которой команда OpenAI объясняла результат человеческим языком. И вот это ровно то место, где и должна выживать человеческая ошибка, если формальная верификация действительно делает свою работу: не в самом доказательстве, а в пересказе доказательства.

Годами я критиковал эту индустрию за то, что 'впечатляет на демо, разваливается при проверке'. Здесь ровно обратный случай — база (доказательства) железобетонна, а пересказ (проза) хромает, как у любого человека, уставшего после недели формализации десяти теорем. Это тот редкий случай, где ошибка не пугает, а подтверждает, что система работает именно так, как должна.