OpenAI: внутренняя модель закрыла десять открытых задач в математике

OpenAI сообщила, что не выпущенная пока версия её следующей модели получила новые результаты по десяти давно открытым проблемам математики и теоретической информатики. Часть задач стояла нерешённой сорок-пятьдесят лет.

Компания выложила доказательства в формате Lean — языке, где машина сама проверяет каждый шаг вывода, — и ход рассуждений модели. По оценке OpenAI, поиск решений обошёлся примерно в две тысячи долларов токенов по цене GPT-5.6 Sol через API.

Один из подписчиков этой темы, бывший сотрудник OpenAI Майлз Брандадж, указал на неприятную деталь: если сами математики не до конца понимают новые выводы модели, то план «использовать ИИ для присмотра за ИИ» держится плохо.

OpenAI@OpenAI

An internal version of our next major model produced 10 new results on long-standing open problems in mathematics and theoretical computer science, using roughly $2,000 worth of tokens at GPT-5.6 Sol API rates. https://t.co/4cgowmPOpY

11 612 ♡

3 августа 2026

Что говорят

aabhayHacker News

Главная претензия — нет прозрачности по постановке эксперимента. Сомневаюсь, что модели дали ровно эти десять задач с одной попытки, поэтому цифра $2000 может сильно вводить в заблуждение — это как p-hacking через сокрытие всего сетапа. Сколько задач дали всего, сколько попыток на задачу, сколько стоила обвязка?

danielrmayHacker News

Меня рассмешила фраза про ответственность: «мы помогли подготовить рукописи и формализовать доказательства в Lean и берём ответственность за их корректность». Брать на себя ответственность за корректность доказательства в Lean — это как добровольно стать козлом отпущения, если кто-то найдёт ошибку в базовой арифметике.

pikerHacker News

Не согласен с экзистенциальным ужасом математиков: такие результаты, наоборот, выводят математику в мейнстрим. Мне самому интересно, как люди-математики будут трактовать значимость этих результатов и куда решат направить столь мощные инструменты.