AI 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 comparator, самостійно підтвердити, що докази бібліотеки відповідають заявленим теоремам. Компанія застерігає, що повна перевірка може займати години; скорочена версія, що охоплює інші два результати, виконується за кілька хвилин.

Де це стоїть серед заяв про формалізацію ШІ

Результат з’явився у році, коли кількість заяв про те, що системи ШІ виконують дослідницьку математику, стрімко зростає, більшість з них базуються на конкурсних балах або коротких доказах. Axiom Math є одним із найактивніших заявників: AxiomProver приписують розв’язання раніше відкритих задач, включаючи роботи, опубліковані компанією у рецензованих журналах, а системи ШІ вже вирішили кілька довготривалих проблем Ердоша. Формалізація 246 — це інший тип результату: не нова теорема, а машинно‑перевірна реконструкція одного з найтехнічно складних доказів у сучасній теорії чисел.

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

Ця різниця важлива для інтерпретації результату. Одноразова перевірка демонструє, що система може впоратися з одним складним доказом. Бібліотека ж демонструє щось ближче до інфраструктури — багаторазового формального інструментарію, на якому можуть будувати інші результати — що є напрямком, у якому розвиваються системи формального доведення, коли вони переходять від розв’язання вправ до перевірки реальної математики. Твердження про можливості тут базується на публічних та відтворюваних артефактах, а не на балу тесту: план, код Lean та задача‑порівнювач, створені так, щоб зовнішні дослідники могли самостійно перевірити докази.

Оно розглядає математику як випробувальний майданчик для більш амбітної мети. Якщо властивості програмного забезпечення — чи завершує програма роботу, чи правильний її вихід для кожного вхідного параметра — можна виразити у вигляді точних математичних тверджень, то системи, створені на базі AxiomProver, могли б формально їх довести, — стверджує він, вказуючи на верифікацію коду, створеного ШІ, який починає керувати інфраструктурою, фінансами та системами безпеки.

«Світ готується працювати на комп’ютерному коді, який ніхто не читав», — сказав Оно. «ШІ вже тут, і ми більше не можемо відводити погляд — формалізація доказів є випробувальним майданчиком для розв’язання, на мій погляд, найважливішого виклику, який ми зустрінемо від ШІ».

Поки що результат є більш вузьким і перевіряним: план, створений 41‑м автором, публічна бібліотека Lean та машинно‑перевірений доказ, що прості числа, розташовані на відстані до 246 один від одного, не вичерпуються — найближчий перевірений сусід гіпотези про близнюкові прості числа та найглибша частина дослідницької математики, яку система ШІ досі перевірила від початку до кінця.