Клод доказал Ферма за 11 дней. Вердикт: SHIP IT.

Что освещается в этом видео

• Клод формализует Великую теорему Ферма в Lean 4
• Chromium sandbox RCE (CVE-2026-85046), активно эксплуатируется, награда $1000
• Шин Джин-со побеждает 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-агента для кодирования. Затем Клод формализовал Великую теорему Ферма, а на той же первой странице корейский гроссмейстер победил сильнейший движок Го на Земле, так что сегодня человечество выиграло один из двух. В этом видео: что на самом деле доказал Клод, сколько это стоило,

0:52 почему математик, потративший на это свою карьеру, говорит, что это ничего не меняет и все равно в восторге, и как человек победил машину в Го. Сегодня пятница, 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: нет, извините, нет нативного 'decide', никакого обмана. Проверка тоже недешева: сборка

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

2:56 цитирую, математически эта работа по сути ничего нам не говорит. Он уже был на 99,9 процента уверен, что теорема верна, и доказательство не добавляет новой математики; оно показывает, что теперь может делать автоформализация, и этой частью он искренне взволнован. Ему дали один миллион фунтов на пять лет; Anthropic потребовалось одиннадцать дней, и расчеты комментатора на салфетке оценивают шесть миллиардов выходных токенов по прейскурантной цене около 300 000 долларов, так что машина была дешевле, если не считать обучение машины, чего никто не делает.

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

3:50 Решающая партия была выиграна с преимуществом в 11,5 очков за 221 ход, удерживая 99-процентную вероятность победы с середины игры, и он забрал домой 250 миллионов вон, около 170 000 долларов, плюс Genesis G90, так что награда за победу над сверхчеловеческим ИИ в 170 раз превышает награду Google за обход песочницы Chrome. Его объяснение: в начале он копировал ходы ИИ и проиграл; он выиграл, строя доску в своём собственном стиле, что является самым полезным советом об ИИ, который я слышал за весь год, и он пришёл из настольной игры. Ещё две строки в The Daily Diff.

4:22 Компилятор Rust React от oxc теперь является нативным в Vite за одним флагом; кодовая база из 1036 файлов сократила время компиляции с 14,3 секунды до 0,81 на этапе компиляции, в основном за счёт удаления Babel из package.json, что также является моей процедурой по уходу за кожей. А IBM запустила Bob, партнёра по кодированию на основе ИИ, который приветствует вас словами «Привет, я Боб», создаёт субагентов, модернизирует код мейнфреймов и поставляет аналитический продукт под названием Bobalytics, так что где-то банк очень взволнован, и никто не читал лицензию.

4:51 Это большая маржа для одной пятницы; если вы предпочитаете читать это, а не слышать, как я говорю, The Daily Diff приходит в ваш почтовый ящик каждое утро — бесплатно на the daily diff dot dev, ссылка ниже. Итак, сегодняшний вердикт: SHIP IT. Ядро говорит да, Buzzard говорит да, математика не изменилась, но способ, которым мы проверяем математику, только что изменился. Это сегодняшний The Daily 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