# Клод даказаў тэарэму Ферма за 11 дзён. Вердыкт: SHIP IT.

Published: 2026-09-07

Клод выдаткаваў 11 дзён і каля 6 мільярдаў токенаў на напісанне 13-мільённага доказу тэарэмы Ферма ў Lean — першага поўнага камп'ютарнага доказу — у той час як матэматык, які фармалізуе яе з 2024 года, кажа, што яна "не гаворыць нам практычна нічога" ў матэматычным плане, і ўсё роўна ў захапленні. У той жа дзень: сусветны № 1 па гульні Го Шын Джын-сеа перамагае KataGo 2:1 з гандыкапам у два камяні. Вердыкт: SHIP IT.

Canonical: https://thedailydiff.dev/be/video/2026-09-04-fermat-lean/

## Што ахоплівае гэта відэа

- Клод фармалізуе Апошнюю тэарэму Ферма ў Lean 4
- RCE ў пясочніцы Chromium (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, памочнік доказу, мог механічна правяраць кожны крок, і Кевін Базард з Імперскага ўніверсітэта ўзначальваў чалавечы намаганняў па выкананні менавіта гэтага з 2024 года; адзін толькі план займае 86 старонак. Даследчык Anthropic Цяньі Пэн накіраваў на гэта дзесяткі агентаў Клода замест гэтага, на платформе пад назвай Prove2Me, якая падтрымлівае DAG тэарэтычных заяў, каб агенты ведалі, што даказваць далей, таму што без гэтага першыя

2:00 роі гублялі след таго, хто што даказваў, што і адбываецца, калі ваш пласт аркестрацыі - гэта regex з маркетынгавым бюджэтам. Праз адзінаццаць дзён каранёвы вузел паказваў PROVED: трынаццаць мільёнаў радкоў Lean, 29 500 прамежкавых тэарэм, каля шасці мільярдаў выходных токенаў з унутранай мадэлі, прыблізна параўнальнай з Claude Fable 5.1. Зборка не праходзіць, калі доказ не грунтуецца выключна на трох стандартных аксіёмах Lean: прабачце, без натыўнага decide, без падману. Праверка гэтага таксама нятанная: зборка з

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

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

3:24 Лепшая дэталь: ліст прыйшоў, калі ён быў на музычным фестывалі ў Уэльсе з адной палоскай 4G, ад імя, якога ён ніколі не чуў, таму ён спісаў гэта як жарт і прачытаў праз тыдзень, што з'яўляецца правільным адказам на любы радок тэмы які змяшчае скразную фармалізацыю. Між тым, людзі ўзялі рэванш. Шын Джын-сео, нумар адзін у свеце па Go, перамог KataGo, самы моцны рухавік Go з адкрытым зыходным кодам, дзве гульні да адной у Сеуле з гандыкапам у два камяні, прыкладна розніца паміж топ-прафесіяналам і пачаткоўцам-прафесіяналам.

3:50 Вызначальнай была перамога з лікам 11,5 ачкоў за 221 ход, утрымліваючы 99 працэнтаў верагоднасці перамогі з сярэдзіны гульні, і ён забраў дадому 250 мільёнаў вон, каля 170 000 долараў, плюс Genesis G90, так што ўзнагарода за перамогу над звышчалавечым AI ў 170 разоў большая за ўзнагароду Google за выхад з пясочніцы Chrome. Яго тлумачэнне: напачатку ён капіяваў хады AI і прайграваў; ён выйграў, будуючы дошку ў сваім уласным стылі, што з'яўляецца самай карыснай парадай пра AI, якую я чуў увесь год, і яна прыйшла з настольнай гульні. Яшчэ два радкі ў The Daily Diff.

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

4:51 Гэта шмат запасу для адной пятніцы; калі вы аддаеце перавагу прачытаць гэта, чым пачуць, як я гэта кажу, The Daily Diff трапляе ў вашу паштовую скрыню кожную раніцу — бясплатна на The Daily Diff dot dev, спасылка ніжэй. Такім чынам, сённяшні вердыкт: SHIP IT. Ядро кажа так, Buzzard кажа так, матэматыка не змянілася, але спосаб, якім мы правяраем матэматыку, толькі што змяніўся. Гэта сённяшні The Daily Diff. Я Ніка з Axrisi.

5:09 Аб'ядноўвайце адказна.

## Крыніцы

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com