Яндекс.Метрика
← Дайджест от 1 августа 2026

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

OpenAI опубликовала отчёт о десяти математических результатах, полученных внутренней версией её следующей модели — Astra. Речь о задачах, которые оставались открытыми десятилетиями: среди них первый явный пример несофической группы (тип абстрактной алгебраической структуры, существование которого двадцать лет было центральным вопросом области) и опровержение гипотезы жёсткости Конна в функциональном анализе.

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

Реакция раскололась. Исследователь Эндрю Гордон Уилсон предсказывает вал доказанных гипотез в ближайшие полгода без заметного влияния на саму математику; Педро Домингос замечает, что теоремы, до которых никому не было дела, становятся событием, когда их доказывает ИИ. Astra ещё не выпущена — по сообщению The Information, Альтман показывал её в Вашингтоне, и она станет первой моделью компании, проходящей новую процедуру государственного согласования перед релизом.

Sebastien Bubeck@SebastienBubeck
yes, nonsofic groups exist: this statement is one of many new beautiful results proved by Astra, our next major model. We're releasing 10 such Astra proofs, complete with lean certificates and CoT walkthroughs for each of them. The results are wide-ranging, from von Neumann
6 033
1 августа 2026
Что говорят
aabhayHacker News
Главная претензия — нет прозрачности по всему эксперименту. Сомневаюсь, что модели просто дали эти десять задач с одной попытки, поэтому цифра в $2000 может вводить в заблуждение — это как p-hacking, когда не раскрывают полную постановку. Сколько всего задач дали? Сколько попыток на задачу? Насколько дорогой была вся обвязка?
danielrmayHacker News
Меня развеселила фраза про авторство: «Мы помогли подготовить рукописи, формализовать доказательства в Lean и берём на себя ответственность за их корректность». Вызваться отвечать за корректность доказательства, проверенного в Lean, — это как добровольно стать козлом отпущения на случай, если кто-то найдёт ошибку в элементарной арифметике.
pikerHacker News
Мне кажется, экзистенциальный ужас математиков неоправдан: наоборот, эти результаты выводят математику в мейнстрим. Я лично жду человеческих интерпретаций и обсуждений значимости таких результатов. Да, выигрывают в основном суперзвёзды, но при этом это отличное время уходить вглубь специализаций, решая, куда направить эти мощные инструменты.