6 октября 2026 года OpenAI опубликовала в репозитории на GitHub математические результаты, полученные внутренней моделью. В репозитории лежат рукописи, вспомогательные артефакты доказательств и формализации на Leanязык программирования, позволяющий проверять математические доказательства компьютером. Каталог содержит 719 рукописей, организованных в 372 семейства; около 42% ключевых результатов формализованы. Средний результат, по оценке OpenAI, потребовал примерно трёх часов вычислений уровня ChatGPT Pro.
Что именно выложили
Помимо PDF-препринтов, в репозитории есть библиотека Lean и каталог формализаций, описывающий доступные формальные доказательства, связанные с ними статьи и конфигурации проверки. Отдельный каталог reasoning_traces содержит сокращённые сводки рассуждений модели — они охватывают семейства 007, 017, 087, 102, 159, 197, 221, 271, 287, 362. В корне репозитория лежат CONTENTS.md, LICENSE, README.md, history.md, overview.pdf и overview.tex.
Формализованы не все результаты: в README прямо сказано, что коллекция включает работы на разных стадиях проверки и не у всех есть сопроводительная формализация. Репозиторий обещают пополнять формализациями по мере их получения, а у неформализованных результатов возможны проблемы, которые обещают быстро исправлять.
Препринты лежат в каталоге preprints отдельными папками. Внутри папки — build, README.md и paper.pdf. Например, работа «Integer multiplication below n log n» датирована 23 сентября 2026 года, её автор указан как OpenAI, а для цитирования приведён BibTeX с ключом OAI:Integer-multiplication-below-n-log-n-September-23-2026. В перечне работ также указаны «The Mézard–Parisi formula for diluted spin glasses» и «Spontaneous magnetization in the quantum Heisenberg ferromagnet».
Как устроена проверка
Проверки в репозитории делятся на три типа: точная арифметика на рациональных числах, интервальная арифметика и формализация на Lean.
Точная арифметика. Скрипт verify.py воспроизводит конечные точные арифметические сертификаты рукописи офлайн. Все арифметические решения выполняются через fractions.Fraction, без чисел с плавающей точкой — в шапке скрипта оговорено, что это не пруф-ассистентпрограмма, которая проверяет доказательства формально, по шагам вывода. Проверки строятся на нескольких примитивах: тождество требует, чтобы переданная разность была равна нулю; скалярное утверждение требует истинности условия; интервальная оценка требует, чтобы все коэффициенты Бернштейначисла, через которые многочлен раскладывается по базису Бернштейна на отрезке или треугольнике были не меньше заданного порога (при строгом режиме — строго больше); треугольный сертификатпроверка, при которой коэффициенты Бернштейна строятся на треугольнике и сверяется точный шаблон нулей строит коэффициенты Бернштейна на треугольнике и сверяет точный шаблон нулей. Для скалярной записи требуется нижняя граница значения, для матричной — границы по минимальному собственному значению и определителю. Отдельно проверяются матричные тождества и монотонность, а также полином синуса, интервальные оценки, кусочные интегралы и сохранённые верхняя и нижняя границы объёма.
Интервальная арифметика. В verify_scalar.py арифметика построена на точных дробях: функция q отклоняет float и возвращает Fraction, а require возбуждает ошибку при ложном условии — намеренно не assert, чтобы проверка работала и под python -O. Полиномы представлены списками коэффициентов: сложение покоэффициентное, умножение — свёртка, норма — сумма модулей коэффициентов. Класс Quartic хранит пару из полинома степени не выше пятой и равномерной ошибки на отрезке [-1,1]; при умножении ошибка оценивается через нормы сомножителей, а нижняя граница вычисляется перебором по коэффициентам и знакам. Ряды заданы таблицами: 11 строк по четыре значения, 6 строк по девять значений, 11 строк по четыре значения и 6 строк по шесть значений. Константы включают ALPHA=3/40, BETA=7/25, S=40/37, GAMMA=3/4, DS=5/17, а бюджеты ошибок — EQ=1/10**8 и EK=8/10**7. Проверка якорей вычисляет число π по формуле Мачина через арктангенсы 1/5 и 1/239, проверяет интервал для θ₀ и якоря Миллсаточные границы для величины, связанной с функцией Миллса, которые служат опорными значениями при проверке. Интервальная арифметика отличается от точной тем, что оперирует не одним точным значением, а парой границ, между которыми значение гарантированно лежит, — это позволяет строго проверять неравенства там, где точное вычисление невозможно.
Рациональная арифметика полиномов. Модуль polynomial.py запрещает коэффициенты с плавающей точкой и хранит только ненулевые члены как Fraction. Деление многочленов точное: при ненулевом остатке или несовпадении произведения частного на делитель с исходным многочленом возбуждается ошибка. Функция reduce_circle убирает зависимость от sin²+cos²−1, заменяя чётные степени синуса через биномиальные коэффициенты. Коэффициенты Бернштейна на отрезке и на треугольнике вычисляются через аффинную подстановку, после чего восстановленный по базису многочлен сверяется с исходным — базисы кэшируются.
Интервальные сертификаты. certificate.py строит сертификаты через рекуррентное вычисление степенных рядов: evolve делает один шаг интегрирования, проверяет априорные границы, рекуррентно вычисляет коэффициенты и добавляет оценку остатка, makeflows выполняет подшаги для набора длин блоков и возвращает матрицы монодромииматрицы, которые показывают, как перенос решения вдоль шага интегрирования меняет его вариации — то есть как малые изменения начальных данных отражаются на результате к концу шага, а check проверяет накопленные нормы и остатки. interval_certificate.py использует библиотеку Arbбиблиотека для строгих интервальных вычислений с произвольной точностью для строгих интервальных вычислений: строит квадратурную сетку из 256 узлов с проверкой положительности весов и того, что их сумма содержит единицу, вычисляет моменты и проверяет границы через сравнение с интервальными константами.
Полнота покрытия
В interval_certificate.py после формирования результата стоят явные проверки покрытия. Они фиксируют, что обработаны ровно ожидаемые узлы, столбцы, матрицы, остатки и знаковые интервалы: например, что множество пар «функция — узел» в остатках совпадает с декартовым произведением двух функций на список узлов, что число центров равно 22, а знаковых интервалов — 84, с распределением 41 и 43 по функциям. В комментарии сказано, зачем это нужно: явные проверки покрытия не дают случайно укороченному прогону выдать статус pass. В результат записываются конкретные числа покрытия, включая 51 конечный узел, 2 матричных знака, 102 пары остатков, 22 знаковых центра и 84 интервала полушага.
Зачем это сделали
OpenAI объясняет публикацию стремлением продвинуть границу человеческого знания и обеспечить дальнейший прогресс в математике. Результаты размещены в GitHub-репозитории с протоколами для правок статей и цитирования, формализации на Lean выложены как часть репозитория, а дополнительные детали о том, как получены результаты, опубликованы ради научной прозрачности и открытости. Компания намерена финансировать серию воркшопов, конференций и специальных программ вокруг понимания крупных результатов, произведённых ИИ.
Результаты получены внутренней frontier-модельюпередовой моделью компании, ещё не выпущенной публично. В README указано, что подавляющее большинство результатов получено одной и той же процедурой с использованием невыпущенной внутренней модели OpenAI. Компания заявляет, что работает над ответственным выпуском модели, породившей эти результаты, и что важно продолжать оценивать внутренние frontier-модели на математике и других науках.
Что это меняет на практике
Проверки можно воспроизвести локально. verify.py по умолчанию пересчитывает результаты и сравнивает их с поставляемым results.json; режим --write пересчитывает и заменяет этот файл рядом со скриптом. Если bundled results.json отсутствует, скрипт требует запустить --write; если пересчитанные результаты не совпадают с bundled, сообщается об ошибке. verify_scalar.py обходится точной арифметикой Fraction из стандартной библиотеки. interval_certificate.py требует внешнюю библиотеку flint с модулями arb, acb, arb_mat, ctx и данные из certificate_data; его входные данные — публичный математический манифест и отображаемые целочисленные таблицы, а сертификат запускается явной командой — импорт модуля его не запускает.
Для Lean-экосистемы совместимость неполная: формализовано около 42% ключевых результатов, часть работ остаётся без сопроводительных формализаций, а репозиторий обещают пополнять. Для дополнительной проверки предусмотрены инструкции ComparatorИнструмент из репозитория openai/math, для которого в README приведены отдельные инструкции по дополнительной проверке формальных доказательств..
Ограничения и открытые вопросы
Авторы прямо оговаривают границы проверок: verify.py воспроизводит конечные точные арифметические сертификаты офлайн, все арифметические решения идут через fractions.Fraction, и это не пруф-ассистент. То есть код проверяет конечные тождества, сертификаты коэффициентов Бернштейна и рациональные границы объёма, но не заменяет систему формального доказательства. В разложении F полное равенство исключает все невыписанные степени, включая нечётные и выше восьмой.
Открытым остаётся статус самой модели: она не выпущена, а доступ к ней для исследовательского сообщества обещан после завершения проверок безопасности.
