Що сталося
1 серпня 2026 року OpenAI опублікувала звіт із розвʼязаннями десяти математичних задач, які лишалися відкритими щонайменше з 2016 року. Розвʼязання отримала внутрішня версія моделі, яку компанія називає Astra — за її формулюванням, це наступне велике сімейство моделей. Публічного релізу в Astra немає, дата й підсумкова назва не оголошені.
Деталі
Задачі охоплюють вісім галузей: геометрію високих розмірностей, теорію кодування, складність арифметичних схем, теорію груп, операторні алгебри, квантову складність, ґраткову криптографію та екстремальну комбінаторику. Одне з доведень встановлює існування не-софічних груп — питання, яке трималося відкритим у теорії груп.
Головна відмінність від попередніх заяв «ШІ розвʼязав математику» — перевірюваність. Кожне доведення модель формалізувала в Lean, мові для машинної перевірки доведень. Це означає, що коректність кожного кроку підтверджує не людина на око й не сама модель, а незалежна програма-верифікатор. Плюс OpenAI виклала розбір ходу міркувань щодо кожної задачі.
Вартість обчислень компанія оцінила приблизно в $2000 за тарифами API для рівня Sol — старшого щабля лінійки GPT-5.6 (оцінка OpenAI на 1 серпня 2026 року).
Ноам Браун, співавтор технології міркувань Astra, окремо відзначив межі результату: компанія пробувала підступитися й до більших проблем, але без успіху — «на жаль, задач тисячоліття поки немає». Математик Томас Блум із Манчестерського університету назвав опубліковане «великою новиною».
Саму Astra описано як систему, що координує кілька агентів на довгій дистанції — годинами й добами — над однією складною задачею. Сем Альтман уже показував її політикам і регуляторам у Вашингтоні. Чи вийде вона під назвою GPT-6, GPT-5.7 чи якось інакше, у компанії не вирішили.
Що це означає
Практику, який сьогодні користується ШІ, це не дає нічого: моделі в доступі немає, ні в API, ні в підписці. Цінність новини в іншому — у способі перевірки. Доведення в Lean можна перевірити в себе за хвилини, тож тут нема чого брати на віру, на відміну від бенчмарків, які вендор рахує сам за своєю методикою.
Кому це важливо вже зараз: дослідникам і всім, хто оцінює, де проходить межа можливостей моделей. Орієнтир за ціною — близько $2000 токенів на десять задач, тобто приблизно $200 за одну відкриту задачу. Це не «дешево», але й не масштаб суперкомпʼютера: можна порівняти з вартістю кількох днів роботи людини.
Обережність тут доречна в одному місці: десять розвʼязаних задач — це не «математику закрито». Відібрано задачі, за якими результат вийшов, а скільки спроб не вдалося, компанія не розкриває. Горизонт — найближчі місяці: доки Astra не зʼявиться в API, повторити результат ззовні ніхто не зможе.
