AxiomProver впервые формально проверил доказательство теоремы о разрыве 246

ИИ-стартап Axiom Math объявил, что его система AxiomProver впервые автоматически проверила формальное доказательство «теоремы 246», результата о разрывах между простыми числами. Теорема утверждает: существует бесконечно много пар простых чисел, отличающихся ровно на 246. Формальная верификация означает, что компьютер построчно перепроверил математически строгую, машиночитаемую версию доказательства; это не стопроцентная гарантия правильности, как показала недавняя демонстрация, баг в самом методе проверки позволил принять ложное, сгенерированное ИИ доказательство (деталей этого случая источник не приводит), но метод считается практически равносильным официальному подтверждению.

Само доказательство теоремы 246 принадлежит не Axiom Math, а коллективу математиков Polymath8b. Путь к нему начался в 2013 году, когда Итан Чжан, ныне профессор университета Сунь Ятсена в Гуанчжоу, впервые доказал, что существует бесконечно много пар простых чисел с ограниченным разрывом, в 70 миллионов. Спустя несколько месяцев профессор Оксфорда Джеймс Мейнард другим методом резко сократил этот разрыв до 600, работа, которая существенно способствовала присуждению ему Филдсовской медали в 2022 году. Затем участники Polymath8b, включая Мейнарда и филдсовского медалиста Теренса Тао (профессора Калифорнийского университета в Лос-Анджелесе), довели разрыв до 246. Это ближайшее из доказанных приближений к нерешённой гипотезе близнецов, которая утверждает, что существует бесконечно много пар простых чисел с разрывом 2; сама эта гипотеза остаётся недоказанной.

По словам основателя Axiom Math математика Кена Оно, теорема 246, «порог человеческих знаний о простых числах» и самое значимое доказательство, которое AxiomProver проверил за год активной работы над множеством задач теории чисел. AxiomProver, автономная мультиагентная система, переводящая математические утверждения в машинопроверяемые доказательства; для теоремы 246 команда собрала переиспользуемую библиотеку результатов о разрывах между простыми числами, где теорема 246, флагманский результат. Сидхартх Хариаран, аспирант Университета Карнеги, Меллон, который ранее руководил ручной частью формализации доказательства Марины Вязовской (Филдсовская медаль 2022 года за задачу плотной упаковки сфер в 8 и 24 измерениях) для конкурента Axiom Math, компании Math, Inc. и её агента Gauss, а теперь стажируется в Axiom Math, говорит, что формализация теоремы 246, более полное и полезное достижение: в отличие от разовой работы над одной задачей, её сделали так, чтобы компоненты годились и для других задач формализации.

Теория чисел, где получен этот результат, лежит в основе всей современной криптографии и кибербезопасности, так что техники формализации могут пригодиться и там. Но Оно видит в проекте более широкую перспективу, проверку ИИ-сгенерированного кода. Если свойства кода (например, завершается ли алгоритм или верен ли результат программы для любого входа) перевести в точные математические утверждения, то технологии на основе AxiomProver подойдут для их формальной формулировки и доказательства. «Мир скоро будет работать на компьютерном коде, который никто не читал, заключает Оно., ИИ уже здесь, и от этого нельзя больше отворачиваться: формализация доказательств, испытательный полигон для решения того, что я считаю важнейшим вызовом, который ИИ поставит перед нами».

Ключевые факты

AxiomProver (Axiom Math) впервые формально проверил доказательство «теоремы 246»: бесконечно много пар простых чисел отличаются на 246, ближайшее доказанное приближение к нерешённой гипотезе близнецов (разрыв 2).
Само доказательство принадлежит коллективу Polymath8b: путь начался с Итана Чжана (разрыв 70 миллионов, 2013 год), продолжился Джеймсом Мейнардом (сократил разрыв до 600, Филдсовская медаль 2022), а до 246 разрыв довели Мейнард и Теренс Тао.
Основатель Axiom Math Кен Оно называет теорему 246 «порогом человеческих знаний о простых числах» и самым значимым из доказательств, которые AxiomProver проверил за год.
Формализация построена как переиспользуемая: команда собрала библиотеку результатов о разрывах между простыми числами, где теорема 246, флагманский результат, а не разовый кейс.
Оно видит в проекте шаг к проверке корректности ИИ-сгенерированного кода той же техникой формальной верификации; при этом сама верификация не даёт стопроцентной гарантии, ранее баг в методе позволил принять ложное ИИ-доказательство.

Почему это важно

AxiomProver впервые формально проверил доказательство теоремы 246, по словам Кена Оно, «порога человеческих знаний о простых числах». Axiom Math формализовала и проверила немало доказательств за год, но именно это, по оценке компании, самое значимое: оно показывает, что автоматическая формальная проверка доказательств такого уровня сложности стала практически осуществимой, а не только теоретически возможной.

Кому это важно

Математикам и специалистам по теории чисел, как новый переиспользуемый ресурс: библиотека результатов о разрывах между простыми числами. Специалистам по криптографии и кибербезопасности, теория чисел лежит в основе большинства современных криптографических схем. Разработчикам и исследователям ИИ-безопасности, которые хотят формально проверять корректность кода, сгенерированного ИИ, а не просто доверять ему на слово.

Как это применить

Формализация сделана переиспользуемой: команда собрала библиотеку результатов о разрывах между простыми числами, где теорема 246, флагманский результат, а её компоненты годятся для других задач формализации. По словам Оно, тот же принцип, перевод точных свойств кода (завершается ли алгоритм, верен ли вывод программы для любого входа) в математические утверждения, в перспективе может лечь в основу формальной проверки корректности ИИ-сгенерированного кода.

Можно ли доверять

Источник, IEEE Spectrum, профильное научно-техническое издание, материал не сатирический. Оценку достижения дают сами участники (Кен Оно, Axiom Math) и Сидхартх Хариаран, аспирант Карнеги-Меллона, который ранее руководил формализацией другого крупного доказательства (Марины Вязовской) для конкурента Axiom Math, компании Math, Inc., а теперь сам стажируется в Axiom Math и участвовал в формализации теоремы 246; по его словам, новая работа более полная и полезная. При этом статья сама оговаривает: формальная верификация, не стопроцентная гарантия правильности доказательства, ранее баг в методе проверки позволил принять ложное ИИ-сгенерированное доказательство (детали этого случая источник не раскрывает). Прошла ли сама работа над теоремой 246 независимое рецензирование математическим сообществом, источник не уточняет.

Риски и подводные камни

Сама гипотеза близнецов (что существуют пары простых чисел с разрывом 2) остаётся недоказанной, теорема 246 лишь ближайшее к ней подтверждённое приближение, а не решение. Источник не называет точную дату завершения проверки теоремы 246 (указано только «ранее в этом году» для отдельной, не связанной с ней работы над доказательством Вязовской). Главный методологический риск, тот же баг формальной верификации: механизм проверки в принципе можно эксплуатировать так, чтобы он принял неверное доказательство, если в конкретной реализации есть ошибка.

«Эта теорема сейчас представляет собой порог человеческих знаний о простых числах.»

— Кен Оно, основатель Axiom Math