На 6 октомври OpenAI публикува хранилище с нови математически резултати, произведени от вътрешен frontier модел. Към много от доказателствата има формализации в Lean, които компютър може да провери стъпка по стъпка. Кой е моделът, OpenAI не казва; резултатите са изброени в хранилището.
Накратко- 6 октомври 2026: OpenAI публикува в GitHub „широк набор“ нови математически резултати от вътрешен модел, който не назовава.
- За много от доказателствата има формализации в Lean, език, на който компютър проверява всяка стъпка. OpenAI обещава още.
- По данни на OpenAI средният резултат е струвал около три часа мислене на ChatGPT Pro. Моделът още не е пуснат; компанията работи по отговорното му пускане.
Три часа. Толкова мислене на ChatGPT Pro е струвал средният резултат от новата математическа партида на OpenAI, по данни на компанията. Числото е едно от нещата, които този път можеш да погледнеш сам.
Фактите: на 6 октомври 2026 г. OpenAI публикува „широк набор нови математически резултати“, произведени от вътрешен
frontier модел, който не назовава. Резултатите са в
GitHub хранилище, с протоколи за ревизии на статиите и за цитиране. Компанията казва, че се е допитвала до независимата Advisory Group on Mathematics and Artificial Intelligence към Institute for Advanced Study и е ползвала нейните съвети и публични препоръки, и че продължава да търси хоствана от общността алтернатива, която отговаря на насоките на комитета. За много от доказателствата в хранилището има формализации в
Lean и OpenAI ще добавя още. Публикувани са и подробности как са получени резултатите: 10 резюмета на разсъжденията на
модела, оценки на изчислението в единици използване на ChatGPT Pro и статистика за броя опитани задачи. По данни на OpenAI средният резултат е използвал изчисление, равно на около три часа мислене на ChatGPT Pro. Компанията ще финансира серия от семинари, конференции и специални програми около разбирането на големи резултати, произведени от AI, и работи по отговорното пускане на модела, който ги е произвел. В README на хранилището OpenAI уточнява още: 722 ръкописа в 372 семейства резултати, около 4000 поставени на модела задачи, резултати на различен етап на проверка; не всички имат формализация в Lean, а някои от неформализираните може да имат проблеми.
Lean превръща проверката на доказателство в работа за машина: пускаш файла и тя казва дали всяка стъпка държи. Остава втората проверка, която машината не прави: дали записаното в Lean е точно въпросът, който математиците питат. Това е наш прочит, не думи на OpenAI.
Lean проверява доказателството. Кой проверява въпроса?
Обявата не изброява резултатите и не назовава модела. Хранилището ги изброява, 722 ръкописа; модела не назовава и то.
Публично вече е проверимото: Lean файловете, десетте резюмета на разсъжденията, оценката на изчислението. Моделът, който ги е произвел, не е. OpenAI казва, че работи по отговорното му пускане, без дата.
Визуалът към статията е генериран код-арт, без чужди изображения.