AI Radar
OpenAI представила результаты моделей по математике, информатике и физике
OpenAI представила созданные моделями доказательства по математике и физике, а также заявленное опровержение гипотезы экспоненциального времени в информатике. Независимая проверка результатов продолжается.
В математической части OpenAI сообщает о доказательстве гипотезы локального сглаживания Согге, связанной с поведением волн. По данным компании, из результата следуют доказательства гипотез Какеи и Стейна. Текст математической работы и его формализация в Lean опубликованы: Lean позволяет записать утверждения и проверить шаги доказательства.
В теоретической информатике компания заявляет об опровержении гипотезы экспоненциального времени, или ETH. Она утверждает, что для определённого класса задач время вычислений неизбежно растёт экспоненциально. OpenAI сообщает, что результат формализован в Lean; его изучает группа исследователей, в которую входят два автора исходной гипотезы. Практически полезные алгоритмы из этого результата пока не следуют.
В физической части речь идёт о предложенных доказательствах существования квантовой хромодинамики и чистой теории Янга – Миллса в четырёх измерениях. Материалы этой части пока не опубликованы; их разбирает группа под руководством Дэвида Гросса. Заявленный результат по теории Янга – Миллса не означает полного решения связанной с ней задачи тысячелетия.
Почему это важно
Для математиков и исследователей алгоритмов проверка этих работ может уточнить статус известных гипотез. Пока заявленное опровержение ETH не даёт готового способа ускорить программы.
Мнение редакции
Мнение редакцииФормализация в Lean позволяет проверять логические шаги доказательства машинным способом. Исследователям теперь предстоит внимательно сопоставить записанные в ней утверждения с исходными научными задачами.
Первоисточники и подтверждения
Подборку проверяет редакция DSML. AI помогает дедуплицировать сигналы и готовить текст, но опубликованный выпуск остаётся редакционным продуктом, а не лентой отдельных каналов.