Проверка доказательств ИИ: Гаусс решает задачу 24D

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

«Эти новые результаты кажутся очень, очень впечатляющими и определенно сигнализируют о некотором быстром прогрессе в этом направлении», — говорит эксперт по ИИ-рассуждению и Принстонский университет постдок Лиам Фаулкоторый не принимал участия в работе.

В своем исследовании, получившем медаль Филдса, Вязовская рассмотрела две версии проблемы упаковки сфер, которая задается вопросом: насколько плотно могут быть одинаковые круги, сферыи т. д., быть упакованы в н-мерное пространство? В двух измерениях соты являются лучшим решением. В трех измерениях оптимальны сферы, сложенные в пирамиду. Но после этого становится чрезвычайно сложно найти лучшее решение и доказать, что оно действительно лучшее.

В 2016 году Вязовская решила проблему в двух случаях. Используя мощные математические функции, известные как (квази)модульные формы, она доказала, что симметричное расположение, известное как E₈ это лучшая 8-мерная упаковкаи вскоре после этого доказал с коллегами, что есть еще одна сферическая упаковка, называемая Решетка пиявки лучше всего работает в 24 измерениях.. Хотя этот результат кажется абстрактным, он потенциально может помочь решить повседневные проблемы, связанные с плотной упаковкой сфер, в том числе коды, исправляющие ошибки используется смартфоны и космические зонды.

Доказательства были проверены математическим сообществом и признаны правильными, что привело к признанию Медали Филдса. Но формальная верификация — способность доказательства быть проверена компьютером — совсем другое дело. С 2022 года многое прогресс было сделано в ходе формальной проверки доказательств с помощью ИИ.

Интуиция приводит к формализации проекта

Несколько лет спустя случайная встреча в Лозанне. Швейцариямежду студентами третьего курса Сидхарт Харихаран и Вязовская возобновила свой интерес к доказательствам упаковки сфер. Хотя Харихаран находился еще на очень раннем этапе своей карьеры, он уже научился формализовать доказательства.

«Формальная проверка доказательства подобна штампу», — говорит Фаул. «Это своего рода добросовестное подтверждение того, что вы знаете, что ваши рассуждения верны».

Харихаран рассказал Вязовской, как он использовал процесс формализации доказательств, чтобы изучить и по-настоящему понять математические концепции. В ответ Вязовская выразила заинтересованность в формализации своих доказательств, в основном из любопытства. При этом в марте 2024 г. Формализация упаковки сфер в Lean проект родился. Лин – популярный программирование язык и «помощник по доказательствам», который позволяет математикам писать доказательства, абсолютная правильность которых затем проверяется компьютером.

Сотрудничество, привлекающее экспертов Бхавик Мехта (Имперский колледж Лондона), Кристофер Биркбек (Университет Восточной Англии, Англия), Сиву Ли (Калифорнийский университет в Беркли) и других, проект включал в себя написание удобочитаемого «чертежа», который можно было бы использовать для отображения различных составляющих 8-мерного доказательства и определения того, какие из них были формализованы и/или доказаны, а какие не были, а затем доказывались и формализовались эти недостающие элементы в бережливом производстве.

«Мы создавали репозиторий проекта около 15 месяцев, когда в июне 2025 года мы открыли публичный доступ», — вспоминает Харихаран, сейчас аспирант первого курса. студент в Университет Карнеги-Меллон. «Затем, в конце октября, мы впервые получили известие от Math, Inc.».

Ускорение искусственного интеллекта

Математика, ООО — стартап, разрабатывающий Gauss, ИИ, специально предназначенный для автоматической формализации доказательств. «Это особый вид языковой модели, называемый агентом рассуждения, который предназначен для чередования как традиционных рассуждений на естественном языке, так и полностью формализованных рассуждений», — объясняет Джесси Хангенеральный директор и соучредитель Math, Inc. «Таким образом, он может выполнять поиск литературы, вызывать инструменты и использовать компьютер для записи кода Lean, делать заметки, запускать инструменты проверки, запускать компилятор Lean и так далее».

Компания Math, Inc. впервые попала в заголовки газет, когда объявила, что Гаусс завершил исследование. Бережливая формализация сильного теорема о простых числах (ПНТ) за три недели прошлым летом, задача, которую медалист Филдса Теренс Тао и Алексей Конторович работал над. Точно так же компания Math, Inc. связалась с Харихараном и его коллегами и сообщила, что Гаусс доказал несколько фактов, связанных с их проектом по упаковке сфер.

«Они сказали нам, что закончили 30 «извините», а это означало, что они доказали 30 промежуточных фактов, которые мы хотели доказать», — объясняет Харихаран. Часть этих извинений была передана команде проекта и объединена с их собственной работой. «Один из них помог нам обнаружить опечатку в нашем проекте, которую мы затем исправили», — добавляет Харихаран. «Так что это было довольно плодотворное сотрудничество».

От 8 до 24 измерений

Но затем последовало радиомолчание. Math, Inc., похоже, потеряла интерес. Однако, пока Харихаран и его коллеги продолжали свою любимую работу, компания Math, Inc. создавала новую, улучшенную версию Гаусса. «Где-то в середине января мы совершили исследовательский прорыв, в результате которого была создана гораздо более сильная версия Гаусса», — говорит Хан. «Эта новая версия воспроизвела наш трехнедельный результат PNT за два-три дня».

Несколько дней спустя новый Гаусс вернулся к формализации упаковки сфер. Используя бесценный ранее существовавший проект и работу, которой поделились Харихаран и его коллеги, Гаусс не только автоформализовал 8-мерный случай, но также нашел и исправил опечатку в опубликованной статье, и все это за пять дней.

«Когда в конце января к нам обратились и сказали, что они это, мягко говоря, закончили, мы были очень удивлены», — говорит Харихаран. «Но, в конце концов, это технология, которая нас очень волнует, потому что она способна совершать великие дела и оказывать замечательную помощь математикам».

Харихаран работал над проверкой доказательства упаковки сфер, когда солнце садилось за Хамершлаг-холлом Карнеги-Меллона.Сидхарт Харихаран

Одна лишь формализация доказательства упаковки 8-мерных сфер объявлено 23 февраляпредставляет собой переломный момент для автоформализации и сотрудничества ИИ и человека. Но сегодня компания Math, Inc. раскрыла еще более впечатляющее достижение: Гаусс автоформализовал 24-мерное доказательство упаковки сфер Вязовской — все его более 200 000 строк кода — всего за две недели.

Между 8- и 24-мерным случаями есть общие черты с точки зрения базовой теории и общей архитектуры доказательства, а это означает, что часть кода из 8-мерного случая может быть реорганизована и использована повторно. Однако у Гаусса не было ранее существовавшего плана работы с этого времени. «И на самом деле это было значительно сложнее, чем 8-мерный случай, потому что было много недостающего исходного материала, который нужно было ввести в эксплуатацию, связанного со многими свойствами решетки Лича, в частности ее уникальностью», — объясняет Хан.

Хотя 24-мерный случай был автоматизированной работой, и Хан, и Харихаран признают большой вклад людей, который заложил основу для этого достижения, рассматривая его как совместную работу людей и ИИ.

Но для Хана это означает нечто большее: начало революционной трансформации в математикагде чрезвычайно масштабные формализации являются обычным явлением. «Раньше программистом считался тот, кто проделывал дырки в картах, но затем процесс программирования стал отделен от материального субстрата, который использовался для записи программ», — заключает он. «Я думаю, что конечным результатом подобных технологий станет свобода математиков делать то, что они умеют лучше всего, а именно мечтать о новых математических мирах».