ИИ Axiom Math проверил теорему о разностях простых чисел 246 в Lean

Axiom Math заявляет, что её система AxiomProver создала машинно‑проверенное доказательство в Lean 4 самого сильного известного результата о разностях между простыми числами: теорему, согласно которой бесконечно много пар простых чисел различаются не более чем на 246. Компания опубликовала результат 17 августа 2026 года как интерактивный формализованный чертёж, в котором указано 41 именованный участник‑математик, инженер и главный исследователь, с первым сообщением IEEE Spectrum о достижении.

Ограничение 246 сейчас является границей человеческих знаний в длительной атаке на гипотезу двойных простых чисел, гипотезу XIX века, согласно которой простые числа, различающиеся ровно на два, встречаются бесконечно. Страница проекта Axiom Math описывает работу как единый формализованный вариант статьи Джеймса Мейнарда 2013 года “Small gaps between primes” совместно с частью последующего проекта Polymath8b, который уменьшил ограничение Мейнарда с 600 до 246. Машинно‑проверенные доказательства организованы в публичную библиотеку Lean — PrimeGapsLib, где теорема о 246 является её флагманским результатом.

«Эта теорема в настоящее время представляет собой границу человеческих знаний о простых числах», — сказал Кен Оно, основатель‑математик Axiom Math.

Формальная верификация означает перевод доказательства в язык, который небольшая доверенная программа, называемая ядром, может проверять построчно. Результат не является абсолютной гарантией — само утверждение должно быть корректно переведено, а проверяющая программа должна быть надёжной — но это устраняет человеческую ошибочность из цепочки. До настоящего времени системы ИИ, соревнующиеся в математических бенчмарках, в основном оценивались по задачам конкурсов с короткими, автономными доказательствами; разрыв между этими результатами и формализацией уровня исследований был значительным, что видно по ранним системам, преуспевавшим в олимпиадной геометрии, при этом исследовательская математика оставалась почти нетронутой.

От 70 млн до 246

Сама гипотеза, точно сформулированная Альфонсом де Полиньяком в XIX веке, остаётся недоказанной. Первый конечный предел любого рода появился в 2013 году, когда Итан Чжан доказал, что бесконечно много пар простых чисел находятся на расстоянии не более 70 млн друг от друга. Спустя несколько месяцев Мейнард представил усовершенствованный метод просеивания и сократил предел до 600 — работа, которая способствовала его получению Филдсовской медали в 2022 году — а сотрудничество Polymath8b, в котором участвовали Мейнард и Терренс Тао, снизило его до 246. Чертёж Axiom Math излагает эту эволюцию как проект, который они намеревались формализовать.

Формализация следует конвейеру, который компания описывает в три этапа. Сначала исследователи записали доказательство как чертёж — каждому определению, лемме и теореме присвоили метку, точное утверждение и список зависимых результатов — создав граф зависимостей, упорядочивший работу. Затем AxiomProver, многопользовательская система компании для математических исследований через формальные доказательства, сгенерировал машинно‑проверяемые доказательства Lean 4, построенные на Mathlib — общественной библиотеке математики, и на PrimeNumberTheoremAnd, существующем проекте формализации под руководством Алекса Конторовича и Тао. Команда Axiom затем проверила сгенерированный код и организовала его в PrimeGapsLib.

Указанные основные результаты библиотеки немного выходят за пределы основной теоремы. Помимо ограничения 246, она формализует ограничение Мейнарда в 600, и включает самостоятельный вызов верификации — построенный только на Mathlib, с пустым местом для доказательства — который позволяет каждому, имеющему инструмент сравнения Lean, независимо подтвердить, что доказательства библиотеки соответствуют заявленным теоремам. Компания предупреждает, что полная проверка может занять часы; сокращённая версия, охватывающая остальные два результата, выполняется за несколько минут.

Где это стоит среди заявлений об ИИ‑формализации

Результат появился в год, когда растут заявления о том, что системы ИИ занимаются математикой исследовательского уровня, большинство из которых опираются на баллы конкурсов или короткие доказательства. Axiom Math является одним из самых активных заявителей: AxiomProver приписывают решение ранее открытых задач, включая работы, опубликованные компанией в рецензируемых журналах, и системы ИИ теперь решили несколько многолетних задач Эрдо́ша. Формализация 246 — это иной тип результата: не новая теорема, а машинно‑проверенная реконструкция одного из наиболее технически сложных доказательств в современной теории чисел.

Ближайшее сравнение — начало этого года, когда Math, Inc. использовала своего агента Gauss для завершения формального доказательства результатов упаковки сфер Марины Вязовской, получивших Филдсовскую медаль, в измерениях 8 и 24. Сидхарт Харихаран, аспирант Carnegie Mellon, который руководил человеческим чертёжом этой формализации и сейчас стажёр в Axiom Math и именованный математический участник проекта 246, утверждает, что новый результат представляет собой более всёобъёмное достижение. По его словам, причина в том, что Axiom построила всё для повторного использования: вместо одноразовой формализации единственного доказательства, PrimeGapsLib — поддерживаемая библиотека результатов о разностях простых чисел, предназначенная поддерживать будущие работы по формализации и исследования.

Это различие важно для восприятия результата. Одноразовая верификация показывает, что система может справиться с одним сложным доказательством. Библиотека демонстрирует нечто ближе к инфраструктуре — повторно используемому формальному механизму, на котором могут базировать другие результаты — что является направлением, к которому движутся формальные системы доказательства, переходя от решения упражнений к проверке реальной математики. Здесь утверждение о возможностях опирается на артефакты, которые являются публичными и повторно исполняемыми, а не на балл бенчмарка: чертёж, код Lean и вызов сравнения, разработанные так, чтобы внешние исследователи могли самостоятельно проверять доказательства.

Оно рассматривает математику как испытательный стенд для более амбициозных целей. Если свойства программного обеспечения — завершение программы, корректность её вывода для любого входа — могут быть выражены в виде точных математических утверждений, то, по его мнению, системы, основанные на AxiomProver, могли бы формально их доказывать, указывая на верификацию кода, генерируемого ИИ, который начинает управлять инфраструктурой, финансами и системами безопасности.

«Мир собирается работать на компьютерном коде, который никто не читал», — сказал Оно. «ИИ уже здесь, и мы больше не можем отводить взгляд — формализация доказательств является испытательным полигоном для решения, как я считаю, самой важной задачи, с которой мы столкнёмся из‑за ИИ».

На данный момент поставка более узкая и проверяемая: чертёж, созданный 41‑м автором, публичная библиотека Lean и машинно‑проверенное доказательство того, что простые числа, различающиеся не более чем на 246, никогда не исчерпываются — ближайший проверенный сосед гипотезы двойных простых чисел и самая глубокая часть исследовательской математики, которую система ИИ пока проверила от начала до конца.