Claude довів Ферма за 11 днів. Вердикт: SHIP IT.

Що охоплює це відео

• Claude формалізує Велику теорему Ферма в Lean 4
• RCE в Chromium Sandbox (CVE-2026-85046), експлуатується в дикій природі, винагорода $1,000
• Шин Джин-сео перемагає KataGo з гандикапом у два камені

Перекладена стенограма

Перекладено з оригінальної англійської розповіді. Доступне аудіо та субтитри контролюються YouTube.

0:00 Ферма сказав, що його чудовий доказ не поміститься на полях, і сьогодні Anthropic опублікував поля: тринадцять мільйонів рядків Lean, у п'ять разів більше, ніж Mathlib, доводячи теорему, у яку кожен математик вже вірив. Було десять-одинадцять у Тбілісі, коли Anthropic опублікував, тому, природно, я не спав. Вчора Google випустив Chrome 152 з дванадцятьма виправленнями безпеки, одна з них – помилка V8, вже експлуатована в дикій природі, і заплатив репортеру тисячу доларів, що менше, ніж седан, до якого ми повернемося пізніше.

0:26 Також вчора Mullvad оголосив, що припиняє роботу свого публічного зашифрованого DNS 2 листопада і платить Quad9, щоб він робив це замість них, а сьогодні вранці Rust React Компілятор став нативним у Vite, тоді як Hacker News виявив IBM Bob, агента AI для кодування. Потім Claude формалізував Велику теорему Ферма, і на тій же першій сторінці корейський гросмейстер переміг найсильніший рушій Go на Землі, тож сьогодні людство виграло один з двох. У цьому відео: що насправді довів Claude, скільки це коштувало,

0:52 чому математик, який провів свою кар'єру над цим, каже, що це нічого не змінює і все одно в захваті, і як людина перемогла машину в Go. П'ятниця, 4 вересня, і це The Daily Diff. Велика теорема Ферма: немає додатних цілих чисел a, b, c, які задовольняють a в степені n плюс b в степені n дорівнює c в степені n для будь-якого n більше 2. Ферма накреслив це на полях близько 1637 року і помер, не показавши своєї роботи, зробивши його першим розробником, який закрив тікет з «працює на моїй машині». Приз у 100 000 золотих марок 1908 року привернув 621 помилковий

1:25 доказ у перший рік, і Ендрю Вайлз нарешті отримав його в 1995 році, на 129 сторінках, які рефері перевіряли місяцями. Формалізація означає переписування цього доказу так, щоб Lean, помічник доведення, міг механічно перевірити кожен крок, і Кевін Баззард з Imperial очолив людські зусилля, щоб зробити саме це з 2024 року; сам лише план займає 86 сторінок. Дослідник Anthropic Тіяні Пенг замість цього направив десятки агентів Claude на нього, на платформі під назвою Prove2Me, яка зберігає DAG заяв теорем, щоб агенти знали, що доводити далі, тому що без неї перші

2:00 зграї втратили слід, хто що доводить, що й відбувається, коли ваш рівень оркестровки – це регулярні вирази з маркетинговим бюджетом. Через одинадцять днів кореневий вузол читав ДОВЕДЕНО: тринадцять мільйонів рядків Lean, 29 500 проміжних теорем, близько шести мільярдів вихідних токенів від внутрішньої моделі, приблизно порівнянної з Claude Fable 5.1. Збірка не вдасться, якщо доказ не базується на трьох стандартних аксіомах Lean: без вибачень, без нативного вирішення, без обману. Перевірка також недешева: збірка

2:29 з нуля займала п'ять з половиною годин на 96 ядрах і 153 гігабайтах оперативної пам'яті, а назви теорем генеруються машиною, тому репозиторій описує себе як написаний для перевірки, а не для читання, що я також описав би як корпоративна Java. Тепер протиріччя. Публікація Anthropic стверджує, що Lean демонструє правильність поза всяким сумнівом. Кевін Баззард, людина, яку випередили, скомпілював репозиторій на 500-гігабайтній машині, яку Anthropic йому позичив, підтвердив, що він перевіряється, а потім написав,

2:56 цитую, з математичної точки зору ця робота по суті нічого нам не говорить. Він вже був на 99,9 відсотка впевнений, що теорема вірна, і доказ не додає нової математики; що він показує, так це те, на що здатна автоформалізація зараз, і ця частина його щиро захоплює. Йому дали один мільйон фунтів за п'ять років; Anthropic витратив одинадцять днів, і підрахунки коментатора на серветці показують, що шість мільярдів вихідних токенів за прейскурантом близько 300 000 доларів, тож машина була дешевшою, якщо не враховувати навчання машини, чого ніхто не робить.

3:24 Найкраща деталь: електронний лист прийшов, коли він був на музичному фестивалі в Уельсі з однією смужкою 4G, від імені, про яке він ніколи не чув, тому він списав це як витівку і прочитав його тиждень потому, що є правильною відповіддю на будь-який заголовок, що містить наскрізну формалізацію. Тим часом люди відігралися. Шин Джин-сео, світовий номер один у Го, переміг KataGo, найсильніший рушій Го з відкритим кодом, дві гри до однієї в Сеулі з двокамінним гандикапом, приблизно така ж різниця, як між топовим професіоналом і новачком-професіоналом.

3:50 Вирішальною була перемога з рахунком 11,5 очок за 221 хід, утримуючи 99 відсотків ймовірності перемоги з середини гри, і він забрав додому 250 мільйонів вон, близько 170 000 доларів, плюс Genesis G90, тож винагорода за перемогу над надлюдським ШІ у 170 разів більша, ніж винагорода Google за втечу з пісочниці Chrome. Його пояснення: на початку він копіював ходи ШІ і програв; він переміг, будуючи дошку у власному стилі, що є найкориснішою порадою щодо ШІ, яку я чув цього року, і вона прийшла з настільної гри. Ще два рядки у diff.

4:22 Компілятор Rust React від oxc тепер є нативним у Vite за одним прапорцем; кодова база з 1036 файлів перейшла від 14,3 секунди до 0,81 секунди на кроці компіляції, здебільшого завдяки видаленню Babel з package.json, що також є моєю рутиною догляду за шкірою. А IBM запустила Bob, партнера зі ШІ-кодування, який вітає вас: "Привіт, я Боб", створює субагентів, модернізує код мейнфреймів, і випускає аналітичний продукт під назвою Bobalytics, тож десь банк дуже схвильований, і ніхто не прочитав ліцензію.

4:51 Це багато для однієї п'ятниці; якщо ви волієте читати це, ніж чути, як я це говорю, The Daily Diff надходить на вашу поштову скриньку щоранку — безкоштовно на thedailydiff.dev, посилання нижче. Отже, сьогоднішній вердикт: SHIP IT. Ядро каже так, Buzzard каже так, математика не змінилася, але спосіб, яким ми перевіряємо математику, щойно змінився. Це сьогоднішній diff. Я Ніко з Axrisi.

5:09 Зливайте відповідально.

Джерела

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com