Пчелиные соты, 24 измерения и нейросеть. Как ИИ проверил главную математическую работу десятилетия
NewsMakerВаш смартфон работает благодаря 24-мерным сферам, а теперь это подтвердил и компьютер.
Когда украинский математик Марина Вязовская получила Филдсовскую медаль летом 2022 года, научное сообщество восприняло событие как историческое. Вязовская стала лишь второй женщиной за 86 лет существования премии. Спустя почти четыре года имя исследовательницы снова оказалось в центре внимания. На этот раз повод связан не с новым доказательством, а с неожиданным союзом математики и искусственного интеллекта: компьютерные системы сумели формально проверить её сложнейшие доказательства.
Речь идёт о знаменитой задаче упаковки сфер. Математики давно пытаются понять, насколько плотно одинаковые шары можно разместить в пространстве. В двумерном мире лучший вариант напоминает пчелиные соты, в трёхмерном — пирамиду из шаров. Дальше задача становится почти неразрешимой. С ростом числа измерений поиск оптимальной конфигурации превращается в одну из самых сложных проблем современной математики.
В 2016 году Вязовская совершила прорыв. Исследовательница доказала, что в восьмимерном пространстве наилучшую упаковку образует симметричная структура, известная как решётка E8. Чуть позже совместно с коллегами математик показала, что в 24 измерениях оптимальную плотность даёт так называемая решётка Лича. На первый взгляд результат кажется чисто абстрактным, однако подобные конструкции лежат в основе кодов коррекции ошибок — технологий, которые используют смартфоны, спутники и космические аппараты для передачи данных без потерь.
Математическое сообщество тщательно проверило доказательства и признало работу безупречной, что и принесло Вязовской Филдсовскую медаль. Но существует ещё один уровень проверки — формальная верификация. В таком подходе компьютер пошагово проверяет каждое логическое утверждение доказательства. Перевести огромный математический текст в форму, понятную машине, крайне трудно, поэтому многие известные доказательства до сих пор не прошли подобную процедуру.
Когда украинский математик Марина Вязовская получила Филдсовскую медаль летом 2022 года, научное сообщество восприняло событие как историческое. Вязовская стала лишь второй женщиной за 86 лет существования премии. Спустя почти четыре года имя исследовательницы снова оказалось в центре внимания. На этот раз повод связан не с новым доказательством, а с неожиданным союзом математики и искусственного интеллекта: компьютерные системы сумели формально проверить её сложнейшие доказательства.
Речь идёт о знаменитой задаче упаковки сфер. Математики давно пытаются понять, насколько плотно одинаковые шары можно разместить в пространстве. В двумерном мире лучший вариант напоминает пчелиные соты, в трёхмерном — пирамиду из шаров. Дальше задача становится почти неразрешимой. С ростом числа измерений поиск оптимальной конфигурации превращается в одну из самых сложных проблем современной математики.
В 2016 году Вязовская совершила прорыв. Исследовательница доказала, что в восьмимерном пространстве наилучшую упаковку образует симметричная структура, известная как решётка E8. Чуть позже совместно с коллегами математик показала, что в 24 измерениях оптимальную плотность даёт так называемая решётка Лича. На первый взгляд результат кажется чисто абстрактным, однако подобные конструкции лежат в основе кодов коррекции ошибок — технологий, которые используют смартфоны, спутники и космические аппараты для передачи данных без потерь.
Математическое сообщество тщательно проверило доказательства и признало работу безупречной, что и принесло Вязовской Филдсовскую медаль. Но существует ещё один уровень проверки — формальная верификация. В таком подходе компьютер пошагово проверяет каждое логическое утверждение доказательства. Перевести огромный математический текст в форму, понятную машине, крайне трудно, поэтому многие известные доказательства до сих пор не прошли подобную процедуру.