Post #695

Команда проекта Sphere Packing объявила о формализации одной из самых сложных теорем современной математики — доказательства того, что оптимальная упаковка сфер в 8-мерном пространстве это решётка E₈ Оригинальное доказательство принадлежит Марине Вязовской — за него она получила Филдсовскую медаль в 2022 году Но формализовать его, то есть перевести в машинно-верифицируемый вид — отдельная задача, которая требует колоссального труда Ключевую роль сыграл Gauss(тут и тут писали о других проектах) — агент автоформализации от компании Mathematics Inc. Основной репозиторий Sphere Packing Gauss самостоятельно выполнил все финальные шаги доказательства в системе Lean, сэкономив команде несколько месяцев работы Доказательство полностью проверено Lean-ядром без единого пропущенного шага AML здесь не помогал, он закрыл задачу, взяв готовую архитектуру, кодовую базу и blueprint от людей и довёл до результата Люди теперь проверяют и дорабатывают код Gauss, а не пишут его сами Это не замена математиков Но это новая модель работы: человек строит концепцию и инфраструктуру, машина реализует