Ещё не выпущенная флагманская модель OpenAI под названием Astra решила десять сложных математических задач, с которыми не могли справиться более 10 лет, а некоторые — более полувека. Компания опубликовала подробное исследование на 249 страницах с доказательствами, а также выложила на GitHub так называемые Lean-сертификаты (под лицензией Apache 2.0). Это формальные, проверенные компьютером доказательства в системе Lean: каждое логическое действие там строго проверено, и счётчик «недоказанных мест» равен нулю. Это означает, что в доказательствах нет пропущенных шагов и ничего не принято «на веру».
Диапазон тем впечатляет: многомерная геометрия, теория кодирования, теория групп, квантовая сложность, решеточная криптография и экстремальная комбинаторика. Итоговая стоимость всей работы, по подсчетам самой компании — около $2000 в токенах по тарифам API GPT-5.6 Sol.
OpenAI выбрала необычный способ анонса: вместо привычных бенчмарков и промо-роликов компания показала проверяемый результат, который любой математик может открыть и посмотреть. Прием сработал. Томас Блум, математик из Манчестерского университета и автор сайта erdosproblems.com, где собраны нерешенные задачи Пола Эрдеша, назвал результат «большой новостью» и добавил, что он более значим майской истории, когда та же лаборатория показала опровержение одной из гипотез Эрдеша про единичные расстояния.
Но восторг не единодушный. Гэри Маркус, давний и последовательный критик генеративного ИИ, назвал анонс «оверсолд» — то есть раздутым сверх реальной ценности. Ученый считает, что эти десять решенных задач не входят в число знаменитых Millennium Prize Problems (семь задач с призом в миллион долларов от Математического института Клэя), и часть из них может оказаться нишевыми даже внутри своих узких областей математики. Ситуацию усложняет фон: в июне математики выпустили Лейденскую декларацию (Leiden Declaration), которую поддержал Международный математический союз — в ней ученые предупреждают, что ИИ-компании используют опубликованные исследования без согласия авторов, обходят рецензирование и подрывают саму систему авторства и доказательства в науке.
Модель, которая все это проделала, официально еще не выпущена. OpenAI не назвала ни дату релиза, ни цену, ни то, выйдет ли Astra как отдельный GPT-6 или как очередной вариант линейки GPT-5. В общий доступ нейросеть попадет только после федеральной процедуры проверки безопасности ИИ. А на это потребуется какое-то время.
Интересно, что ИИ-компании начинают отходить от привычных сравнений по бенчмаркам, где новые модели сопоставляют с предыдущими версиями и решениями конкурентов. Вместо этого они показывают более наглядные результаты: например, математические доказательства, которые либо проходят строгую формальную проверку, либо нет. Для компании, которую часто критикуют за завышенные ожидания от её моделей, это редкий случай, когда заявления полностью совпадают с проверяемыми фактами — вплоть до каждой строки кода в Lean. Следующим важным этапом станет официальный релиз Astra, когда математики смогут оценить не отдельные задачи, а возможности модели в целом.
