» ИИ самостоятельно завершил формализацию теоремы Филдсовского уровня Дата публикации:24.02.2026, 19:14 70 70 Скопировать Поделись с друзьями! Команда проекта Sphere Packing объявила о формализации одной из самых сложных теорем современной математики — доказательства того, что оптимальная упаковка сфер в 8-мерном пространстве это решётка E₈.

Оригинальное доказательство принадлежит Марине Вязовской — за него она получила Филдсовскую медаль в 2022 году.

Но формализовать его, то есть перевести в машинно-верифицируемый вид — отдельная задача, которая требует колоссального труда.
Ключевую роль сыграл Gauss(тут и тут мы писали о других проектах) — агент автоформализации от компании Mathematics Inc. 

Основной репозиторий Sphere Packing.

Gauss самостоятельно выполнил все финальные шаги доказательства в системе Lean, сэкономив команде несколько месяцев работы. Доказательство полностью проверено Lean-ядром без единого пропущенного шага.

ИИ здесь не помогал, он закрыл задачу. Взял готовую архитектуру, кодовую базу и blueprint от людей и довёл до результата. Люди теперь проверяют и дорабатывают код Gauss, а не пишут его сами.
Это не замена математиков. Но это новая модель работы: человек строит концепцию и инфраструктуру, машина реализует.