Штучний інтелект вирішив чотири складні для людей завдання – AxiomProver розробив та підтвердив докази стародавніх математичних питань – новини у сфері технологій.

Система AxiomProver надала докази для давніх математичних гіпотез.

Стартап Axiom повідомляє, що їхній штучний інтелект AxiomProver за останні кілька тижнів створив кілька нових математичних доказів. Це стосується доказів, пов’язаних з різними аспектами теорії чисел та алгебраїчної геометрії. Як зазначає компанія, ці результати вказують на зростаючі можливості штучного інтелекту в задачах, що вимагають складного міркування, передає Wired.

Хоча штучний інтелект поки що не подолав найвідоміші математичні виклики, система Axiom за останні тижні знайшла рішення для кількох задач, які роками ставили експертів у безвихідь. Ці досягнення демонструють стабільний прогрес математичних здібностей ШІ, який дедалі активніше застосовується науковцями для перевірки гіпотез та пошуку нових ідей. 

“Я вважаю, що штучний інтелект стане новим інтелектуальним інструментом — або, можливо, більш доречно буде сказати “інтелектуальним партнером” — відкриваючи нові горизонти для математичних досліджень”, — підкреслив математик Давей Чен.

Один із доказів стосується гіпотези, над якою п’ять років тому працював Чен разом з математиком Квентіном Гендроном. Тоді їм не вдалося обґрунтувати ключову формулу з теорії чисел, і вони подали свою ідею лише як гіпотезу.

Нещодавно Чен обговорив цю проблему з математиком Кеном Оно, який приєднався до Axiom. Наступного дня Оно представив доказ, згенерований системою AxiomProver, після чого результат був доопрацьований та опублікований на arXiv.

“Після цього все стало на свої місця природним чином”, — зазначив Чен. За його словами, інструмент штучного інтелекту виявив зв’язок із числовим явищем, відомим ще з XIX століття.

AxiomProver повністю самостійно довела гіпотезу Фела, яка стосується сизигій, або математичних виразів, де числа організовані в алгебрі. Вона базується на формулах математика Шрініваси Рамануджана, знайдених понад 100 років тому в його блокноті. Експерти, зокрема професор Гарварду Скотт Комінерс, вражені не лише автоматизацією процесу, а й “елегантністю та красою” знайденого рішення.

Ще два результати стосуються ймовірнісних моделей у теорії чисел та методів, розроблених у контексті доведення Великої теореми Ферма. У компанії наголошують, що йдеться не про найвідоміші відкриті задачі, але про проблеми, які роками залишалися без розв’язання.

“Математика — це справді чудовий полігон і пісочниця для реальності. Ми дійсно вважаємо, що існує багато важливих випадків використання з високою комерційною цінністю”, — заявила генеральна директорка Axiom Каріна Хонг.

Підхід Axiom поєднує великі мовні моделі з власною системою AxiomProver, яка спеціалізується на логічному мисленні. Головною перевагою є використання мови Lean для автоматичної перевірки доказів, що відрізняє цей інструмент від звичайного штучного інтелекту. Це дозволяє системі не лише шукати готові відповіді в базах даних, а й генерувати нові, математично обґрунтовані рішення.

Раніше Google DeepMind оголосила про “історичне досягнення” у сфері штучного інтелекту. Модель Gemini 2.5 за 30 хвилин розв’язала надскладну задачу з гідродинаміки, яка виявилася непосильною для учасників-людей. 

Водночас дослідження організації ORCA, проведене наприкінці 2025 року, поставило під сумнів надійність штучного інтелекту в математичних обчисленнях. Тестування п’яти провідних моделей — Gemini, Grok, DeepSeek, ChatGPT, Claude — показало, що в середньому чат-боти помиляються у 40% випадків.