OpenAI показала модель, яка не просто переказує відомі теореми, а пропонує нові математичні аргументи. 1 серпня 2026 року компанія опублікувала десять результатів щодо відкритих задач у геометрії, теорії кодів, складності обчислень і криптографії. Частина з них, за заявою OpenAI, закриває питання, над якими математики працювали роками.
У центрі роботи — Astra, внутрішня версія наступної великої моделі OpenAI. Спробувати її в ChatGPT поки не можна. Проте компанія відкрила рукописи, пояснення міркувань і формальні сертифікати Lean, тому розмова не зводиться до красивої пресконференції.
Що саме зробила модель OpenAI Astra
OpenAI тестувала Astra на давніх задачах, відповідь на які не була відома під час навчання моделі. Вона отримувала постановку проблеми, шукала можливий шлях і формувала математичний аргумент. Люди після цього готували рукописи, перевіряли виклад і допомагали перевести докази у формальну систему.
Список охоплює десять напрямів. Серед них — нові межі для пакування сфер у просторах великої розмірності, покращення для бінарних і сферичних кодів, конструкція не-софічних груп, спростування гіпотези Конна про жорсткість та результати для задачі найближчого вектора, пов’язаної з постквантовою криптографією.
Навіть людям із математичною освітою складно однаково глибоко оцінити всі десять робіт. Тому важливий не перелік складних назв, а процес: модель запропонувала аргументи, люди перетворили їх на рукописи, а Lean перевірив логічну конструкцію на рівні формальних кроків.
Як перевіряли математичні докази Astra
Рукопис перевіряє не лише красива відповідь
Мовна модель може впевнено написати помилковий доказ. У математиці одна непомітна підміна умови руйнує десятки сторінок подальших міркувань. Саме тому OpenAI не обмежилася текстом, який «схожий на наукову статтю».
Після пошуку розв’язання аргументи оформлювали в рукописи за участі людей і тієї ж моделі. OpenAI також опублікувала для кожної роботи окреме пояснення ходу міркувань. Воно допомагає зрозуміти ідею, але саме по собі не є гарантією правильності.
Lean перевіряє логічні кроки
Lean — це система формалізації математики. У ній твердження й докази записують так, щоб комп’ютер міг перевірити кожен логічний перехід. Якщо десь використано неоголошене припущення або висновок не випливає з попередніх кроків, перевірка не пройде.
Для десяти результатів OpenAI підготувала Lean-сертифікати. Це сильніший рівень контролю, ніж звичайна вичитка тексту, але не чарівна печатка істини. Формальна перевірка підтверджує коректність записаного доказу відносно заданих аксіом і визначень. Вона не вирішує автоматично, наскільки результат новий, правильно поставлена задача чи доречна математична інтерпретація.
Які задачі вдалося просунути
Результати можна умовно розділити на три групи.
- Геометрія й комбінаторика. Сюди входять пакування сфер, гіпотеза Ергарта та багатоколірні числа Рамсея.
- Теорія обчислень. Astra запропонувала нові нижні межі для арифметичних схем і результати щодо квантового паралельного повторення.
- Алгебра та криптографія. Опубліковано роботи про не-софічні групи, гіпотезу Конна і складність наближення задачі найближчого вектора.
OpenAI формулює рівень внеску обережно: деякі роботи розв’язують проблему, інші дають суттєвий прогрес. Остаточну оцінку має дати незалежна математична спільнота після читання рукописів, перевірки новизни та порівняння з попередніми роботами.
Це важлива різниця. Формально правильний аргумент ще треба помістити в контекст галузі. Модель могла знайти відомий шлях в іншому записі, пропустити сильніший результат або використати визначення, яке змінює сенс задачі.
Скільки коштував математичний експеримент
За оцінкою OpenAI, токени, витрачені на пошук усіх десяти розв’язань, коштували б приблизно 2 000 доларів за актуальними тарифами API GPT‑5.6 Sol. Це оцінка обчислень, а не ціна Astra і не вартість повного дослідницького проєкту.
До бюджету не включена робота людей: вибір задач, підготовка середовища, перевірка результатів, оформлення рукописів і формалізація у Lean. Для університету саме ці етапи можуть бути дорожчими за виклики моделі.
Astra зараз недоступна через ChatGPT або публічний API. Науковцям, які хочуть працювати з доступними інструментами OpenAI, варто подивитися на програму ChatGPT для науковців. Вона дає відібраним дослідникам безкоштовний доступ до GPT‑5.6, Codex і Deep Research, але не обіцяє доступу до внутрішньої Astra.
Що може повторити український дослідник
Повторити сам експеримент Astra без моделі й обчислювального бюджету не вийде. Проте його робочий процес можна використати вже зараз.
- Вибрати вузьке твердження. Не просити ШІ «зробити відкриття», а дати точну постановку, визначення та відомі обмеження.
- Вимагати альтернативні підходи. Нехай модель запропонує кілька шляхів і окремо покаже слабкі місця кожного.
- Перевірити джерела вручну. Пошук літератури потрібен для новизни, а не лише для підтвердження зручної відповіді.
- Формалізувати критичну частину. Lean, Coq або Isabelle можуть перевірити логіку там, де помилка найдорожча.
- Залучити профільного фахівця. Модель не замінює рецензента, який бачить контекст галузі.
Для відкритого й локальнішого процесу можна також розглянути OpenScience. Такий варіант потребує більше технічного налаштування, зате дає контроль над моделями, кодом і даними.
Чому авторство ШІ стало окремою проблемою
OpenAI прямо пише, що було б неправильно приписати людині доказ, математичну ідею якого повністю створила модель. Компанія бере відповідальність за підготовку й коректність опублікованих матеріалів, але вказує Astra як джерело аргументів.
Це незручне, але корисне формулювання. ШІ не може нести юридичну або академічну відповідальність як автор. Водночас приховувати його реальний внесок теж нечесно. Для університетів це означає потребу фіксувати, які частини роботи запропонувала модель, що перевірила людина і якими інструментами підтверджено результат.
Публікація Astra не доводить, що математик став зайвим. Вона показує іншу зміну: пошук кандидатів на доказ може ставати машинним, а людська робота зміщується до постановки задачі, контролю новизни, формальної перевірки та пояснення сенсу результату.
Як читати результати Astra без математичної спеціалізації
Починати з усіх десяти рукописів поспіль не потрібно. Виберіть одну задачу й спочатку прочитайте коротке пояснення OpenAI: що було відомо раніше, який бар’єр заважав просунутися і яку нову ідею запропонувала модель. Після цього відкрийте сам рукопис і знайдіть формулювання головної теореми. Навіть якщо технічний доказ лишається складним, стане зрозуміло, що саме змінилося.
Далі корисно подивитися на три окремі шари перевірки. Перший — чи відповідає рукопис заявленій задачі. Другий — чи пройшла формалізація Lean. Третій — як результат оцінюють незалежні дослідники з цієї галузі. Лише разом вони дають нормальну картину.
Не слід сприймати запис міркувань моделі як точний журнал її внутрішньої роботи. Це підготовлене пояснення, корисне для читача, але воно не доводить, що система рухалася до відповіді саме таким шляхом. Для оцінки результату важливіший відтворюваний доказ, а не драматична історія «як ШІ думав».
Якщо тема цікавить із практичного боку, можна взяти одну вже відому теорему й попросити доступну модель запропонувати кілька доказів, а потім порівняти їх із підручником. Це безпечніший навчальний експеримент: правильна відповідь відома, тому легше побачити, де модель скорочує кроки, вигадує посилання або використовує приховане припущення.
