Как сообщает Хабр, ИИ-агент Gauss помог завершить перевод на формальный язык Lean доказательства оптимальной упаковки одинаковых шаров в восьми измерениях. Само доказательство появилось в 2016 году, а спустя десять лет удалось довести его до машиночитаемого вида.

Задача об упаковке сфер знакома каждому по апельсинам на прилавке: интуитивно плотная укладка кажется очевидной, но строгое доказательство оптимальности в восьми измерениях потребовало десятилетий. Формализация в Lean означает перевод рассуждений на язык, который проверяет компьютер, — это отдельная трудоёмкая работа.

По данным источника, к моменту подключения ИИ люди уже проделали огромную подготовительную работу. Именно на этом фундаменте агент Gauss и смог завершить формализацию.

В сентябре 2026 года OpenAI объявила, что её новая модель решила задачу тысячелетия Навье — Стокса. Но там речь идёт о поиске неизвестного доказательства, а не о формализации готового. Заявление вызвало вопросы о корректности результата и самостоятельности ИИ — это уже другая история.

Источник: Telegram: Хабр

#ии в математике#lean#формализация#упаковка сфер#gauss
Понравился материал?
Подписывайтесь — так вы не пропустите новые.
RSS-лента

Комментарии 3

Будьте вежливы — это делает обсуждение лучше
ИК
Ирина К.
Читаю и не понимаю: агент реально что-то доказал или просто добил формализацию, которую люди почти закончили? В статье как-то размыто.
DP
dmitry_p
Разница принципиальная. В статье же прямо сказано: подготовку делали математики, а Lean-доводка — это огромный, но всё же технический труд. Не надо путать это с доказательством с нуля.
Р
РедакцияРедакция
Именно так: доказательство 2016 года существовало, Gauss завершил его перевод на Lean. Это не открытие нового результата, а машиночитаемая проверка готового — тем не менее шаг серьёзный.