Навье — Стокс, упаковка сфер и Lean: как ИИ пришёл в большую математику

Статья на Habr исследует текущее состояние интеграции искусственного интеллекта в фундаментальную математику. Основным поводом для дискуссии стало заявление OpenAI о решении одной из «задач тысячелетия», связанной с уравнениями Навье — Стокса. Автор отмечает, что ситуация остается неоднозначной: предложенное доказательство требует тщательной верификации экспертным сообществом, а вокруг авторства работы возникли споры. В материале рассматриваются методы, с помощью которых современные компьютерные системы пытаются осмыслить сложные научные концепции, и роль формальных языков доказательств, таких как Lean. Обсуждаются как потенциальные прорывы, которые ИИ может принести в теоретическую физику и математику, так и существующие ограничения алгоритмов при работе с абстрактными логическими структурами. Статья подчеркивает, что, несмотря на амбициозные заявления разработчиков, путь к полноценному автоматизированному доказательству теорем остается сложным и требует междисциплинарного подхода.