AI Radar
Внутренняя модель OpenAI Astra получила десять результатов в математике и теоретической информатике, включая задачи, остававшиеся открытыми десятилетиями. Компания приложила формализации доказательств в Lean, но сами результаты ещё нуждаются в проверке научным сообществом.
Среди заявленных достижений — первый явный пример несофической группы, опровержение гипотезы жёсткости Конна, доказательство квантовой теоремы о параллельном повторении для общих двухигровых систем и гипотезы Эрхарта об объёме. Astra также получила первое с 1978 года улучшение общей верхней оценки плотности упаковки сфер и решила задачу Эрдёша №183 о многоцветных числах Рамсея. Это не вариации школьных олимпиадных задач, а вопросы из абстрактной алгебры, функционального анализа, дискретной геометрии и теории сложности, над которыми ранее работали профессиональные математики.
По данным OpenAI, модель самостоятельно нашла ключевые аргументы, а затем перевела доказательства в Lean — формальную систему, способную машинно проверить корректность каждого логического шага. Вместе с сертификатами опубликована рукопись объёмом 249 страниц; стоимость успешных запусков оценивается примерно в $2000 по тарифам Sol API. При этом формальная проверка не заменяет содержательной экспертизы: специалистам предстоит проверить исходные постановки, соответствие формализаций заявленным теоремам и научную новизну построений.
Подробностей об архитектуре Astra пока мало. Её описывают как внутреннюю мультиагентную модель для продолжительной работы над сложными задачами; публичного релиза нет, и OpenAI не называет систему GPT-6. Сообщается и о неудачных попытках решить другие задачи, поэтому десять опубликованных результатов нельзя считать показателем гарантированной эффективности на произвольной открытой проблеме.
Если доказательства выдержат независимую проверку, ценность результата будет не только в ответах, но и в полном цикле от поиска идеи до машинно проверяемой формализации. Для математиков это потенциально новый исследовательский инструмент, однако оценивать его полезность следует по воспроизводимости, доле неудачных запусков и качеству новых методов, а не только по числу выбранных успешных задач.
DSML editors review the selection. AI helps deduplicate signals and draft the text; the published edition remains an editorial product, not a feed of individual channels.
