Команда из Math, Inc. завершила формальное доказательство задачи упаковки сфер в 8 и 24 измерениях. Они подтвердили, что решетки E8 и Leech — самые плотные возможные размещения сфер в этих пространствах.

Ранее эти результаты доказала Марина Вязовская вместе с коллегами. За это Вязовская получила Медаль Филдса — важнейшую награду в математике. Math, Inc. сделали первую формализацию такого высокого уровня доказательства в этом веке.

Задача упаковки сфер спрашивает: как плотно можно уложить одинаковые сферы в n-мерном пространстве. Решена она была только в 1, 2, 3, 8 и 24 измерениях. Особенно сложно было доказать случаи 8 и 24, и для этого потребовалась сложная комбинация геометрии, теории чисел и анализа.

Math, Inc. использовали свой инструмент Gauss для полной автоматизации формализации доказательства. На 8 измерениях автоформализация заняла 5 дней, тогда как вручную это заняло бы полгода. На 24 измерениях — всего две недели. За это время Gauss сам искал и доказывал нужные факты по теории модульных форм, геометрии и анализу.

Объем формализации вырос до около 200 000 строк кода — это огромный проект, который обычно занимает годы работы людей. Теперь формализация математики может ускориться, сделав знания доступными для поиска и автоматического анализа.

Math, Inc. приглашает желающих попробовать Gauss в раннем доступе на официальном сайте. Это шаг к будущему, где сложные математические доказательства будут проверяться автоматически и быстрее.

Подробнее о проекте и результатах можно посмотреть по ссылке: Sphere Packing — Math, Inc.