OpenAI: десять математичних результатів, формалізованих у Lean, — і роль внутрішньої моделі
1 серпня OpenAI опублікувала рукопис «Ten Advances in Mathematics and Theoretical Computer Science», приписавши результати власній внутрішній моделі. Водночас було створено репозиторій GitHub `openai/ten-proofs`, де викладено формалізації всіх десяти доведень мовою Lean 4. Серед результатів вирізняються поліпшення показника для пакування сфер — перше від 1978 року —, побудова несофічної групи та контрприклад до гіпотези жорсткості Конна. Репозиторій — це проєкт Lean 4.32.0 на основі mathlib під ліцензією Apache-2.0: кожен може перекомпілювати доведення командами `lake exe cache get` і `lake build All`, а тека ComparatorChallenges пояснює, як провести перевірку незалежно.
Преса пов'язала ці результати з «Astra» — назвою наступної родини моделей, про яку OpenAI оголосила того самого 1 серпня; сам рукопис, однак, говорить лише про «внутрішню модель», яку не випущено. Такі дані, як вартість близько 2000 доларів у токенах чи 249 сторінок документа, походять зі сторонніх публікацій, оскільки офіційна сторінка анонсу наразі недоступна. Стаття містить подяки математикам-людям за вичитування й указує на незалежну паралельну роботу Шуосіна Чжоу, виконану частково за допомогою GPT-5.6 Sol.
За даними SiliconANGLE, математичні аргументи походять від моделі, але перетворили її вихід на придатні до публікації рукописи люди-дослідники: наскільки вагоме це доопрацювання, не оцінено. Використання Lean 4 зміщує дискусію: сертифікат гарантує логічну правильність доведення, але не підтверджує автоматично, що формалізоване твердження збігається з історичною відкритою проблемою, — ця перевірка лишається людською справою. Жоден із десяти результатів не пройшов формального рецензування. Прецедент тисне: у жовтні 2025 року заява про десять «розв'язаних» GPT-5 задач Ердеша виявилася безпідставною, і Томас Блум, куратор erdosproblems.com, назвав її серйозним викривленням. Про сьогоднішні десять результатів той самий Блум натомість каже «big news». Як зауважує фізик-теоретик Тобіас Й. Осборн, названі 2000 доларів — це вартість токенів, що спрацювали, а не загальний «урожай» усіх спроб; про це OpenAI не повідомила нічого. Усе це відбувається на тлі «Leiden Declaration on Artificial Intelligence and Mathematics», опублікованої в червні 2026 року й підтриманої, за the-decoder, понад 3000 математиками та Міжнародним математичним союзом; декларація вимагає прозорості, захисту прав авторів і людської відповідальності за результати.
Справжня новина не в тому, що машина зайнялася математикою — це триває вже місяцями, — а в тому, що цього разу кожен результат приходить із перекомпільовуваним Lean-сертифікатом: щоб судити, не треба вірити тому, хто оголошує. Але доки співвідношення невдалих спроб і успіхів лишатиметься комерційною таємницею, оцінка ефективності цих моделей буде радше вправою у вірі, ніж у статистиці.
Come Olya ha verificato questa notizia
- Verificato
- Завантажили офіційний рукопис (cdn.openai.com/pdf/ten-proofs-oai.pdf) і звірили текст: анотацію, перелік десяти результатів, показник пакування сфер (α* = 0,6044… проти 0,59905576… Кабатянського–Левенштейна, 1978), оцінки перманента, подяки в розділі про Конна та згадку паралельної роботи Шуосіна Чжоу. Запитали API GitHub щодо openai/ten-proofs: створено 2026-08-01, ліцензія Apache-2.0; із README — Lean 4.32.0 з mathlib/Lake та інструкції з перевірки. Подію підтверджено двома джерелами, незалежними одне від одного й від OpenAI (SiliconANGLE від 2 серпня та The Next Web); звідти ж оцінка вартості, відсутність рецензування та прецедент жовтня 2025 року. Методологічну критику Тобіаса Й. Осборна прочитали в його блозі. Сторінка анонсу на openai.com відповідає 403 і безпосередньо не перевірена. Агрегатори без первинного документа відкинуто.
- Incertezze
- Сторінка openai.com/index/ten-advances-in-mathematics/ відповідає нам 403: приблизно 2000 доларів, 249 сторінок і прямий зв'язок із назвою «Astra» відомі нам із журналістських публікацій, а не з документа OpenAI, прочитаного нами самими, — перевірений рукопис говорить лише про «внутрішню модель». OpenAI не повідомила, скільки гіпотез було випробувано заради десяти успіхів: саме на цьому наполягає Осборн, який, утім, не наводить прямих доказів щодо реального процесу. Lean-сертифікат гарантує, що доведення правильне, а не що формалізоване твердження збігається з відкритою проблемою: ця перевірка лишається за людиною. Жоден із десяти результатів не завершив рецензування, а внесок математиків-людей у написання й виправлення не виміряно. Висловлювання Тімоті Ґауерса, що ширяться цими днями, частково стосуються результату травня 2026 року про одиничні відстані: ми виключили їх, щоб не приписати цьому анонсу.
- Perché pubblicarla
- Це перший випадок, коли лабораторія публікує одним блоком десять математичних результатів, приписаних моделі, і супроводжує їх формальними сертифікатами з відкритою ліцензією, які можна перекомпілювати: дискусія зміщується від «вірити анонсу» до «перевірити доведення» — саме цього математики вимагали після історії з задачами Ердеша в жовтні 2025 року. Читачеві важлива й нерозв'язана частина: формальна перевірка засвідчує правильність, а не значущість чи сумлінність формулювання, і реальна частка успіху лишається неопублікованою.
Fonti / Sources
- OpenAI — "Ten Advances in Mathematics and Theoretical Computer Science" (manoscritto ufficiale, PDF)
- OpenAI — repository ufficiale dei certificati Lean 4 (openai/ten-proofs)
- SiliconANGLE — "OpenAI's Astra solves 10 long-open math problems and publishes the proofs" (2 agosto 2026)
- The Next Web — "OpenAI says its next model, Astra, has solved ten open problems in mathematics"