ИИ завершил формализацию доказательства теоремы Филдсовского уровня

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