Новий математичний прорив ШІ: Astra розв'язала задачі, над якими вчені працювали десятиліттями

04 серпня 2026 р. 08:40

04 серпня 2026 р. 08:40

Невдовзі після попереднього математичного прориву компанія OpenAI представила результати роботи нової моделі Astra, яка, за даними компанії, розв'язала десять відкритих математичних задач, що залишалися нерозв'язаними десятиліттями. Усі отримані докази супроводжуються машинною перевіркою в системі Lean та знаходяться у відкритому доступі. Дослідники називають це важливим кроком для використання штучного інтелекту в науці, хоча частина експертів закликає не поспішати з висновками, передає Forbes .

За оцінкою OpenAI, вартість отримання цих результатів становила близько 2000 доларів. Роботу опублікували 1 серпня разом із 249-сторінковою збіркою розвʼязань. Головною особливістю проєкту стали машинно перевірені сертифікати для кожного результату, які OpenAI опублікувала у відкритому доступі на GitHub.

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

Astra розв'язала десять складних математичних задач із різних галузей, зокрема теорії груп, високовимірної геометрії, теорії кодування, квантової складності, криптографії на ґратках та екстремальної комбінаторики. Серед отриманих результатів — побудова конструкції, що підтверджує існування несофічних груп, розв'язання проблеми, пов'язаної з гіпотезою жорсткості Коннеса, покращення верхньої межі щільності упаковки сфер у високих вимірах, яка залишалася незмінною з 1978 року, а також три задачі з відомого каталогу відкритих проблем, складеного математиком Полом Ердешем.

Це вже другий гучний результат моделі Astra. У травні OpenAI повідомляла, що вона спростувала гіпотезу одиничної відстані Ердеша — задачу дискретної геометрії, яка залишалася відкритою близько 80 років.

Результати позитивно оцінили низка відомих математиків. Лауреат медалі Філдса Тім Говерс заявив, що без вагань рекомендував би ці доведення до публікації у провідному математичному журналі, а згодом разом із вісьмома колегами, серед яких Нога Алон, підготував окрему статтю з поясненням доказів у більш доступній для математиків формі. Томас Блум, який веде каталог задач Ердеша, назвав серпневі результати “великою новиною” та зазначив, що вони можуть виявитися навіть важливішими за попередній результат щодо гіпотези одиничної відстані.

Водночас реліз не залишився без критики. Фахівці звертають увагу, що саме OpenAI обирала, які результати оприлюднювати, а заявлена сума у 2000 доларів стосується лише успішних запусків моделі, а не всіх спроб отримати правильний результат.

Крім того, дослідники зазначають, що співробітники OpenAI брали участь у підготовці наукових статей і формалізації доведень. Також модель Astra поки що недоступна стороннім дослідникам, тому незалежно відтворити процес отримання результатів неможливо — можна лише перевірити вже опубліковані докази.

Один із найвідоміших критиків сучасного ШІ Ґері Маркус назвав реліз “дивовижним, але надзвичайно переоціненим”. Частина математиків також вважає, що після детальнішого аналізу не всі десять задач матимуть однакову наукову вагу.

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

У OpenAI вважають, що така схема може мати значення далеко за межами математики. Подібні механізми вже використовуються під час проєктування мікросхем, у криптографії, перевірці апаратного забезпечення та критично важливого програмного забезпечення, де можливість автоматично підтвердити правильність результату часто є важливішою за швидкість його отримання.

Тим часом у галузі математики не відстають і моделі компанії Anthropic. Штучний інтелект Claude Fable 5 у співпраці з науковцями знайшов імовірний контрприклад до гіпотези Якобіана, яка залишається нерозв'язаною з 1939 року. Модель згенерувала математичну конструкцію, що порушує умови глобальної оборотності поліноміального відображення, але ця робота ще очікує на офіційне рецензування та публікацію.

Технології