Штучний інтелект не просто розв’язував математичні задачі — OpenAI показала, що з цього вийшло. Компанія опублікувала 722 рукописи, створені внутрішньою моделлю ШІ, а частину математичних доказів перевела у формат, який може перевірити комп’ютер. Роботи охоплюють теорію чисел, геометрію, теоретичну інформатику та математичну фізику. Але найцікавіше тут не сама кількість матеріалів, а спроба зробити результати ШІ доступними для незалежної перевірки. Що саме опублікувала OpenAI 6 жовтня 2026 року OpenAI відкрила публічний репозиторій із математичними результатами свого внутрішнього frontier-моделю. У ньому зараз 722 рукописи, об’єднані у 372 дослідницькі родини. Одна «родина» може містити основний результат, додаткові роботи, наслідки або альтернативні докази однієї математичної ідеї. Тому 722 рукописи не означають 722 абсолютно незалежні відкриття. Модель залишилася внутрішньою — OpenAI її не називає і поки не опублікувала. Компанія лише зазначає, що саме ця система використовувалася для роботи з відкритими математичними проблемами. повідомляє NNews із посиланням на OpenAI. ШІ отримав близько 4000 математичних задач Масштаб експерименту вражає не лише кількістю опублікованих рукописів. За даними OpenAI, під час оцінювання моделі їй запропонували приблизно 4000 математичних задач. Результати потім відбирали, об’єднували у дослідницькі напрямки та оформлювали у вигляді рукописів. У середньому на один результат витрачалося обчислення, еквівалентне приблизно трьом годинам режиму «thinking» у ChatGPT Pro. Це важливий нюанс: йдеться не про те, що модель вирішила всі 4000 задач. Опублікована колекція — це відібрані результати, які OpenAI вважала достатньо значущими для включення до каталогу. Найцікавіше — математику намагаються перевірити машиною Саме тут у цій історії з’являється Lean. Lean — це мова програмування та система формалізації, за допомогою якої математичний доказ можна записати у формі, придатній для перевірки комп’ютером. Якщо спростити, звичайний математичний текст можна уявити як довгий ланцюг тверджень: з цього випливає це, з нього — наступне і так далі. Lean дозволяє формально описати такий ланцюг, після чого комп’ютер перевіряє, чи справді кожен крок відповідає заданим правилам. OpenAI опублікувала формалізації багатьох доказів і планує додавати нові. Але це не означає, що всі 722 роботи вже пройшли таку перевірку. Сама OpenAI прямо зазначає, що результати перебувають на різних етапах верифікації, а частина рукописів поки не має Lean-формалізації. Деякі неформалізовані результати можуть містити проблеми. Які проблеми досліджував ШІ У колекції є результати з дуже різних галузей. Серед них — дослідження властивостей числа π, задачі теорії складності, арифметичних прогресій, різні математичні гіпотези, питання геометрії, квантових систем та математичної фізики. OpenAI окремо опублікувала скорочені пояснення міркувань моделі для 10 дослідницьких родин. Серед них — робота з ірраціональністю π, NP-складністю, гіпотезами Маллера, квантовим ферромагнетизмом Гейзенберга та релятивістськими рівняннями Власова—Максвелла. Це важливо ще й тому, що йдеться не лише про стандартні задачі з підручників. Модель перевіряли на відкритих дослідницьких проблемах, де відповідь не була заздалегідь відома як звичайна вправа. Чим це відрізняється від звичайного «ШІ розв’язав задачу» У математиці красивого пояснення недостатньо. Модель може сформулювати переконливий доказ, який насправді містить помилку. Для людини така помилка іноді захована всередині десятків сторінок складних міркувань. Формалізація змінює сам принцип перевірки: частину логічних кроків можна передати комп’ютеру. Водночас Lean не робить автоматично правильною будь-яку математичну роботу. Він перевіряє формалізований доказ відповідно до заданих правил. А питання про те, чи правильно сформульована сама теорема, наскільки важливий результат і як він співвідноситься з попередніми дослідженнями, все одно залишається справою математиків. Що це означає для науки Головна зміна може бути не в тому, що ШІ тепер «замінив математиків». OpenAI фактично демонструє інший сценарій: модель генерує математичні результати, а дослідники отримують документи, вихідні матеріали та в окремих випадках формальні докази, які можна перевіряти й розвивати далі. Компанія також опублікувала інформацію про версії робіт, виправлення та правила цитування. Це дозволяє відстежувати зміни, якщо автори виявлять помилки або доповнять результати. При цьому не варто сприймати всі 722 рукописи як уже підтверджені наукові відкриття. Частина результатів ще потребує формальної перевірки та оцінки фахівців. 💡 Цікаво знати OpenAI опублікувала не лише самі математичні роботи. Для 10 дослідницьких родин компанія також надала скорочені описи того, як модель підходила до відповідних задач. Це окремий шар інформації: формальний доказ показує, чи витримує математична конструкція перевірку, а опис міркувань дає дослідникам уявлення про те, як модель прийшла до результату. ❓ Головне питання: чи означає це, що ШІ вже робить математику краще за людей? Ні, такого висновку з опублікованих матеріалів робити не можна. OpenAI показала масштабний експеримент із внутрішньою моделлю та оприлюднила його результати, але частина робіт ще перебуває на різних етапах перевірки. Крім того, сама компанія не стверджує, що всі опубліковані результати є остаточно підтвердженими математичними відкриттями. Поки правильніше говорити про інше: ШІ вже можна використовувати для пошуку та розробки складних математичних результатів, а формальні системи на кшталт Lean дають спосіб перевіряти значну частину таких результатів набагато жорсткіше, ніж звичайний текстовий аналіз. І саме це робить реліз OpenAI незвичайним. Важливо не лише те, скільки математики згенерувала машина, а й те, що вперше такий масштаб роботи намагаються представити у форматі, придатному для систематичної перевірки та подальшої роботи математиків.