Найновіша інференсна модель OpenAI, яка одночасно представила десять захопливих математичних досягнень.
Включаючи:
- Вперше доведено існування несофічних груп (Non-sofic groups);
- Надано нові нижні межі схем (Circuit lower bounds);
- Подолано межу складності останньої задачі про найближчий вектор (Closest Vector Problem, CVP);
- А також теорема про паралельне повторення з двома гравцями та експоненційним спаданням (Quantum parallel repetition).
Найбільше для доцента Колумбійського університету Генрі Юена важливо останнє —
У 2016 році Юен досяг значного прогресу у цьому питанні, але не вирішив його повністю. Протягом 10 років він постійно зазнавав невдач, і навіть місяць тому він знову спробував досягти остаточного доведення за допомогою ChatGPT 5.5, але отримав мізерні результати.
А ІІ легким ударом ноги на плечі відправив м’яч у ворота.
Доведено правильно, але люди не зрозуміли
Кілька днів тому Ліцзе Чен надіслав чернетку статті Генрі Юену та ще кільком людям.
Тоді життя було напружене, і він не міг глибоко вивчати. Зараз стаття вже опублікована. Він не може тримати це в собі — має що сказати.
Теорема про квантове паралельне повторення (Quantum parallel repetition theorem) — це галузь, якою Генрі Юен глибоко займався протягом кількох років у часи навчання в аспірантурі, і яка є його найбільш власним досягненням.
Генрі Юен, нинішній доцент кафедри комп’ютерних наук Срівані при Колумбійському університеті
Він пам’ятає ті вечори, проведених у кав’ярнях, пізні ночі за робочим столом та безліч вихідних, які мали б бути відпочинком, коли він повторно розбирав і вивчав класичну теорему паралельного повторення Рана Раза.
Він хотів вирішити квантову версію цієї теореми, через що не міг заснути і весь час вертівся. Він «з’їв» тонни математичних інструментів і нарешті успішно довів поліноміальне зменшення.
https://arxiv.org/pdf/1604.04340
Що важливіше, він набув впевненості, нарешті усвідомив свої можливості й довів, що дійсно здатний вирішити ті (хоча б частину) проблеми, які теж цікавлять інших.
Він вважає, що цей доказ від OpenAI, мабуть, правильний, оскільки вже існує формалізований доказ у Lean. Але щоб зрозуміти цей новий доказ, Генрі Юену знадобиться трохи часу.
Хоча новий доказ справді продовжує з того місця, де закінчився попередній, ІІ вийшов за межі його початкової стратегії доведення, застосувавши деякі техніки та методи, які, можливо, вже були відомі дослідникам у галузі операторної теорії та функціонального аналізу.
Крім захоплення, першим відчуттям Юена було розчарування — від стилю написання статті.
Він сказав, що цей документ звучить як написаний штучним інтелектом: довгі вступи, що нікуди не ведуть, а ключові моменти — як магія, що залишає в читача повний розпач.
Доведення від OpenAI цікаве у читанні, але також трохи непросте.
Він спочатку чітко висуває проблему, а потім раптово стрибає до напрямку «використання пре-розв’язання для знаходження правильної очищення», майже не залишаючи жодних логічних етапів між ними.
Потім йде серія досить незвичайних обчислень матричної ентропії, які довго розраховуються, і нарешті повідомляють вам: цей шлях працює.
Але він не пояснює, звідки взялася та найважливіша крок, та інтуїція.
А найбільш тонкий, найбільш вимагаючий креативності хід — використання перетворення Ульмана для розширення простору операторів — мав стати найбільш захопливим кульмінаційним моментом усього доведення, але його було викинуто AI як пісок, без попередження та без пояснень у четвертому розділі.
Правильний доказ, але прихована найважливіша ідея.
Він сподівається, що OpenAI витратить кілька додаткових підказок, щоб добре впорядкувати цей текст.
Ще болісніше — другий рівень: проходження перевірки Lean не означає розуміння.
Машина може забезпечити бездоганність кожного кроку міркування, але на питання «чому цей підхід працює», «що він означає в більш широкій теоретичній картині» та «де ще його можна застосувати» — Lean не може відповісти жодного.
Юен відкрито сказав, що ще не зовсім засвоїв цей доказ.
Відповідь була перед ним, але він мусив, наче читаючи статтю нефахівця, рядок за рядком відновлювати інтуїцію, яку ІІ не висловила.
Так, існує доказ Lean. Але це лише формалізація, що не означає, що я це зрозумів. Щоб справді засвоїти, мабуть, потрібно лише час.
Так, ШІ розширив межі людського розуміння, але потім що? Що залишилося від насолоди та сенсу досліджень? Якщо ШІ вирішить усі його нав’язливі проблеми, що йому залишиться?
Питання виникають одне за одним. Але він все більше переконувався в одному: математикам не буде ніколи нудно — їм потрібно буде не лише підкорити ці інтелектуальні велетні, а й перекласти їхній жаргон зрозумілою мовою.
AI «спростував» столітній математичний гіпотезу — виявилася обманом! Lean також не є скринею
На минулому тижні Рамана Кумар за допомогою 300 рядків Lean спростував найвідомішу нерозв’язану математичну гіпотезу — гіпотезу Коллатца (Collatz conjecture).
Він задає дуже просте питання: маючи додатне ціле число, повторюйте дві правила — якщо число парне, діліть його на 2; якщо непарне, множте на 3 і додавайте 1 — чи зупиниться цей процес завжди на 1, незалежно від початкового числа?
Ти можеш порахувати:
Ця гіпотеза стверджує, що незалежно від того, яке додатне ціле число ви виберете, ви завжди потрапите в цикл 4→2→1.
З моменту, коли математик Лотар Коллатц запропонував цю проблему в 1937 році, ніхто не зміг довести її істинність, ніхто не знайшов зворотного прикладу.
Його назвав математик Пол Ердеш: «Математика ще не готова до таких проблем», а член Американської національної академії наук, математик Джеффрі Лагаріас вважає: «Це надзвичайно складна проблема, яка повністю виходить за межі сучасної математики».
Якщо це буде спростовано, це буде вибуховою новиною для математичного світу.
На жаль, через три дні цей формальний доказ у Lean був визнаний недійсним, оскільки він насправді використовував нижчий рівень вразливості в ядрі Lean.
Даніель Сельсам з OpenAI, з використанням штучного інтелекту, спеціалізованого на кібербезпеці, допоміг Lean FRO провести аудит ядра.
В результаті вони виявили не одну дірку в ядрі Lean!
Майже одночасно професор математики Університету Ратгерс та консультант організації Lean Project Alex Kontorovich опублікував пост із нагадуванням: не сприймайте Lean як універсального перевірника.
Він прямо вказав на слабке місце — семантичне вирівнювання (Semantic Alignment).
Навіть якщо ядро Lean бездоганне, Lean відповідає лише за компіляцію коду. Хто забезпечує, що ваші «визначення» у коді збігаються з «інтуїтивними намірами» людини у природній мові?
Єдине, що може підтвердити Lean: код успішно компілюється, і формальна логіка бездоганна. Але він абсолютно не перевіряє більш критичне питання: чи відповідає це формальне твердження саме тій теоремі, яку ви хочете довести?
Теорему доведено правильно, але умову переписано з помилкою — Lean все одно дає зелений сигнал.
А цю проблему з вирівнюванням неможливо вирішити лише за допомогою комп’ютера.
У доповіді на ICM 2026 Конторович відзначив: найбільша слабка сторона формалізованої математики — не в «правильному виведенні», а в «правильному формулюванні». Остаточний контроль все ще повинен здійснювати людський експерт.
Рівень Liquid Tensor Experiment, який став легендарним, досягався завдяки майже параноїчному ручному перевірці кожного математичного визначення дослідниками.
Порівнявши слова двох професорів, можна зробити висновок: штучний інтелект може доводити, машини можуть перевіряти, але розуміння та контроль залишаються за людиною.
Нарешті, ще одна чутка щодо моделей AI-виведення:
Джерела:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Цей матеріал надійшов із офіційного аккаунту WeChat «Новий розум», автор: ASI Апокаліпсис; редактор: Девід