OpenAI обяви Astra: 10 решени задачи за $2000

На 1 август OpenAI официално назова следващия си голям модел — Astra — и го представи не с бенчмаркове, а с математика. В публикацията Ten advances in mathematics and theoretical computer science компанията описва десет нови резултата по задачи, по които не е имало напредък поне десетилетие, а в повечето случаи значително по-дълго. Всичко е постигнато от вътрешна, непусната още версия на модела, а сметката за токените — около $2000 по тарифите на Sol в API-то (приблизително €1740).

Какво точно е решено

Списъкът е публикуван като 249-страничен ръкопис, придружен от машинно проверими сертификати в Lean 4 за всеки резултат. Кодът е в хранилището openai/ten-proofs в GitHub под лиценз Apache-2.0 и се компилира с Lean 4.32.0 и mathlib.

Сред десетте резултата са:

• Първата явна конструкция на несофична група — въпрос, отворен откакто Михаил Громов въвежда понятието „софичност“ през 1999 г.
• Контрапример към хипотезата за ригидност на Кон за групови фон Нойманови алгебри.
• Доказателство на хипотезата на Ерхарт за обемите на изпъкнали тела с единствена вътрешна решетъчна точка.
• Подобрени асимптотични горни граници за плътността на пакетиране на сфери, стигащи до прага на Кон–Елкис, плюс експоненциално по-силни граници за двоични и сферични кодове.
• Нови долни граници за сложността на пресмятане на перманента, включително граница от порядъка n⁴/log n за формули.
• Експоненциално паралелно повторение за двуиграчови квантови игри и резултат за твърдостта на апроксимация при задачата за най-близкия вектор в решетка — тема, която опира директно до постквантовата криптография.
• Свръхекспоненциални долни граници за многоцветните числа на Рамзи, с което пада задача 183 от списъка на Ердьош, както и контрапримери в екстремалната теория на графите.

Себастиен Бубек, който ръководи математическите изследвания в OpenAI, определи резултатите просто като „красиви“. Ноам Браун добави и уговорката: „За съжаление, засега без задачи за милениума“ — шестте оставащи задачи на института Клей, всяка с награда от 1 млн. долара, остават отворени, макар той да смята, че повече изчислителна мощност би ги доближила.

Снимка: the-decoder / Epoch AI

Защо Lean сертификатите имат значение

Основното възражение срещу досегашните „AI доказателства“ беше практическо: проверката им отнема на човек повече време, отколкото самото решаване. Формализацията в Lean заобикаля този спор — компилаторът или приема доказателството, или не. Това не гарантира, че формулировката на теоремата е интересна или коректно записана, но премахва въпроса дали в средата на 30 страници има скрита логическа дупка.

Тук е и границата на прозрачността. Както отбелязва Саймън Уилисън, OpenAI е публикувала и отделен PDF, в който моделът реконструира как е стигнал до всяко доказателство, но липсват самите промптове и каквито и да е данни за неуспешните опити. Сметката от $2000 покрива десетте успеха; колко е струвало всичко останало, не се знае.

Реакциите в гилдията са смесени

Ако си спомняте първите сигнали за Astra отпреди дни, тогава спорът беше за архитектурата. Сега е за професията.

Обзор на the-decoder описва три ясно различими лагера. Абхишек Саха смята днешните модели за „поне толкова добри, колкото солиден и неуморим докторант“ и разказва как е свършил за един ден с GPT-5.5 Pro работа, която преди е отнемала седмици. Теренс Тао говори за „голямата математика“ — съвместна работа, в която хората поемат творческата част, а машините — техническата черна работа, и предупреждава, че областта влиза в турбулентен период, подобен на кризата в основите ѝ от началото на XX век. Кирвин Хампшър, автор на есето „The Dark Night of Mathematics“ от юли, нарича самата Лайденска декларация „добре заглушен вик“.

Снимка: the-decoder

Има и институционален конфликт. През юни Лайденската декларация, подкрепена от Международния математически съюз, предупреди точно срещу това: AI компании, които обявяват математически резултати чрез прес съобщения, вместо да минат през рецензиране. OpenAI пък заявява, че да се припише човешко авторство на тези доказателства „би представило погрешно и приноса на системата, и природата на истинската човешка интелектуална работа“.

Какво следва

Astra още няма дата за пускане и дори не е ясно дали ще излезе като GPT-6, като междинна версия или като отделен клас модели. Резултатите ще минат през нормалния филтър на общността — рецензиране, обобщения, опити за подобряване — и едва след месеци ще стане ясно кои от десетте са наистина важни и кои са добре свършена техническа работа.

Дотогава числото, което си струва да запомните, не е десет, а две хиляди. Ако сметката за десет доказателства наистина е под цената на един лаптоп, ограничението пред машинната математика вече не е бюджетът, а въпросът кой задава правилните въпроси.