Клод доказа теоремата на Ферма за 11 дни. Присъда: SHIP IT.

Какво обхваща този видеоклип

• Клод формализира последната теорема на Ферма в Lean 4
• Chromium sandbox RCE (CVE-2026-85046), експлоатиран в дивата природа, награда от 1000 долара
• Шин Джин-сео побеждава КатаГо с хендикап от два камъка

Преведен препис

Преведено от оригиналния английски разказ. Наличните аудио и субтитри се контролират от 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 Tianyi Peng насочи десетки агенти на Клод към него вместо това, на платформа, наречена Prove2Me, която поддържа DAG от теореми твърдения, така че агентите знаят какво да доказват след това, защото без нея първите

2:00 рояци изгубиха следа кой какво доказва, което се случва, когато вашият слой за оркестрация е regex с маркетингов бюджет. Единадесет дни по-късно коренният възел гласеше ДОКАЗАНО: тринадесет милиона реда Lean, 29 500 междинни теореми, около шест милиарда изходни токена от вътрешен модел, приблизително сравним с Claude Fable 5.1. Компилацията се проваля, освен ако доказателството не се основава точно на трите стандартни аксиоми на Lean: без съжаление, без родно решение, без измама. Проверката също не е евтина: едно

2:29 изграждане от нулата отне пет часа и половина на 96 ядра и 153 гигабайта RAM, а имената на теоремите са машинно генерирани, така че хранилището описва себе си като написано за проверка, а не за четене, което е и как бих описал корпоративната 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, така че наградата за побеждаване на свръхчовешки AI е 170 пъти по-голяма от наградата на Google за пробив на Chrome sandbox. Неговото обяснение: в началото той копирал ходове на AI и загубил; той спечелил, като изградил дъската в собствен стил, което е най-полезният съвет за AI, който съм чувал през цялата година, и той дойде от настолна игра. Още два реда в дифа.

4:22 Компилаторът Rust React от oxc вече е вграден във Vite зад един флаг; кодова база от 1036 файла премина от 14,3 секунди на 0,81 в стъпката на компилация, главно чрез изтриване на Babel от package.json, което е и моята рутина за грижа за кожата. И IBM стартира Боб, AI партньор за кодиране, който ви поздравява с „Здравейте, аз съм Боб“, създава подизпълнители, модернизира мейнфрейм код, и изпраща аналитичен продукт, наречен Bobalytics, така че някъде някоя банка е много развълнувана и никой не е прочел лиценза.

4:51 Това е голям марж за един петък; ако предпочитате да прочетете това, отколкото да ме чуете да го казвам, дифът пристига във входящата ви кутия всяка сутрин – безплатно на daily diff dot dev, линк по-долу. И така, днешната присъда: SHIP IT. Ядрото казва да, Бъзърд казва да, математиката не се промени, но начинът, по който проверяваме математиката, току-що се промени. Това е днешният диф. Аз съм Нико от 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