Klauss pierādīja Fermā 11 dienās. Spriedums: NOSŪTĪT.

Ko aptver šis video

• Klauss formalizē Fermā pēdējo teorēmu Lean 4 valodā
• Chromium smilškastes RCE (CVE-2026-85046), izmantots dabā, 1000 $ atlīdzība
• Šins Dzin-seo uzvar KataGo ar divu akmeņu handikapu

Tulkotais transkripts

Tulkojums no oriģinālā angļu stāstījuma. Pieejamais audio un subtitri tiek kontrolēti no YouTube.

0:00 Fermā teica, ka viņa brīnišķīgais pierādījums neietilptu malā, un šodien Anthropic publicēja malu: trīspadsmit miljoni rindu Lean valodā, piecas reizes lielāks par Mathlib, pierādot teorēmu, kurai katrs matemātiķis jau ticēja. Tbilisi bija desmit līdz vienpadsmit, kad Anthropic publicēja, tāpēc, protams, es biju nomodā. Vakar Google izlaida Chrome 152 ar divpadsmit drošības labojumiem, viens no tiem bija V8 kļūda, kas jau tika izmantota dabā, un samaksāja reportierim tūkstoš dolāru, kas ir mazāk nekā sedans, pie kura mēs vēlāk nonāksim.

0:26 Arī vakar Mullvad paziņoja, ka 2. novembrī slēdz savu publisko šifrēto DNS un maksās Quad9, lai tas darītu to vietā, un šorīt Rust React kompilators nonāca Vite, kamēr Hacker News atklāja IBM Bob, AI kodēšanas aģentu. Pēc tam Klauss formalizēja Fermā pēdējo teorēmu, un tajā pašā priekšlapā korejiešu lielmeistars uzvarēja spēcīgāko Go dzinēju uz Zemes, tāpēc šodien cilvēce izdarīja viens no diviem. Šajā video: ko Klauss patiesībā pierādīja, ko tas maksāja,

0:52 kāpēc matemātiķis, kurš visu savu karjeru veltīja šim, saka, ka tas neko nemaina un tik un tā ir sajūsmā, un kā cilvēks uzvarēja mašīnu Go spēlē. Ir piektdiena, 4. septembris, un šis ir The Daily Diff. Fermā pēdējā teorēma: nav pozitīvu veselu skaitļu a, b, c apmierina a pakāpē n plus b pakāpē n ir vienāds ar c pakāpē n jebkuram n virs 2. Fermā ap 1637. gadu to uzrakstīja malā un nomira, neparādot savu darbu, padarot viņu par pirmo izstrādātāju, kurš slēdza biļeti ar darbiem manā mašīnā. 1908. gada balva 100 000 zelta marku apmērā piesaistīja 621 nepareizu

1:25 pierādījumu pirmajā gadā, un Endrjū Vailss beidzot to ieguva 1995. gadā, 129 lapaspusēs, kuru pārbaude tiesnešiem prasīja mēnešus. Formalizēšana nozīmē šī pierādījuma pārrakstīšanu, lai Lean, pierādījumu palīgs, var mehāniski pārbaudīt katru soli, un Kevins Buzzards no Imperial ir vadījis cilvēku darbu, lai to darītu tieši kopš 2024. gada; pats plāns ir 86 lapas. Anthropic pētnieks Tiani Pengs novirzīja desmitiem Klausa aģentu uz to tā vietā uz platformas Prove2Me, kas uztur teorēmu DAG (virzīto aciklisko grafu) apgalvojumus, lai aģenti zinātu, ko pierādīt tālāk, jo bez tā pirmās

2:00 spieti zaudēja izpratni par to, kurš ko pierāda, kas notiek, ja jūsu orkestrēšanas slānis ir regex ar mārketinga budžetu. Vienpadsmit dienas vēlāk saknes mezgls rādīja PIERĀDĪTS: trīspadsmit miljoni rindu Lean valodā, 29 500 starpposma teorēmas, aptuveni seši miljardi izvades žetonu no iekšējā modeļa, kas aptuveni salīdzināms ar Claude Fable 5.1. Veidošana neizdodas, ja pierādījums nav balstīts tieši uz Lean trim standarta aksiomām: nē, atvainojiet, nav vietējās izlemšanas, nav krāpšanās. Tā pārbaude arī nav lēta: no

2:29 nulles veidošana aizņēma piecarpus stundas uz 96 kodoliem un 153 gigabaitiem RAM, un teorēmu nosaukumi ir mašīnģenerēti, tāpēc repozitorijs sevi raksturo kā rakstītu pārbaudei, nevis lasīšanai, ko es arī aprakstītu kā uzņēmuma Java. Tagad pretruna. Anthropic ieraksts saka, ka Lean nešaubīgi demonstrē pareizību. Kevins Buzzards, vīrs, kuru pārspēja, apkopojoja repozitoriju uz 500 gigabaitu mašīnas, ko Anthropic viņam aizdeva, apstiprināja, ka tas pārbauda, un pēc tam rakstīja,

2:56 citējot, matemātiski šis darbs mums būtībā neko neatklāj. Viņš jau bija 99,9 procentu pārliecināts, ka teorēma ir patiesa, un pierādījums nepievieno jaunu matemātiku; tas, ko tas parāda, ir tas, ko autoformalizācija var darīt tagad, un par šo daļu viņš patiesi ir sajūsmā. Viņam tika dota viens miljons mārciņu piecu gadu laikā; Anthropic aizņēma vienpadsmit dienas, un komentētāja aptuvenā aprēķina rezultātā seši miljardi izvades žetonu ir par saraksta cenu apmēram 300 000 dolāru, tātad mašīna bija lētāka, ja vien neskaita mašīnas apmācību, ko neviens nedara.

3:24 Labākā detaļa: e-pasts pienāca, kamēr viņš bija mūzikas festivālā Velsā ar vienu 4G signāla iedaļu, no vārda, ko viņš nekad nebija dzirdējis, tāpēc viņš to norakstīja kā blēdību un izlasīja to nedēļu vēlāk, kas ir pareizā atbilde uz jebkuru temata rindu kas satur pilnīgu formalizāciju. Tikmēr cilvēki atguva vienu uzvaru. Šins Džinseo, pasaules pirmā vieta Go spēlē, uzvarēja KataGo, spēcīgāko atvērtā koda Go dzinēju, divas spēles pret vienu Seulā ar divu akmeņu handikapu, aptuveni starpība starp augstākā līmeņa profesionāli un iesācēju profesionāli.

3:50 Izšķirošā bija uzvara ar 11,5 punktiem 221 gājienā, saglabājot 99 procentu uzvaras varbūtību no spēles vidusdaļas, un viņš mājās aizveda 250 miljonus vonu, aptuveni 170 000 dolāru, plus Genesis G90, tātad atlīdzība par supercilvēka AI pārspēšanu ir 170 reizes lielāka nekā Google atlīdzība par Chrome smilškastes izbēgšanu. Viņa paskaidrojums: sākumā viņš kopēja AI gājienus un zaudēja; viņš uzvarēja, veidojot dēli savā stilā, kas ir visnoderīgākais padoms par AI, ko es esmu dzirdējis visu gadu, un tas nāca no galda spēles. Vēl divas rindas izmaiņās.

4:22 Rust React kompilators no oxc tagad ir dabiski integrēts Vite aiz viena karoga; 1036 failu koda bāze kompilācijas solī samazinājās no 14,3 sekundēm līdz 0,81 sekundei, galvenokārt izdzēšot Babel no package.json, kas ir arī mana ādas kopšanas rutīna. Un IBM palaida Bob, AI kodēšanas partneri, kas jūs sveic ar "Sveiki, esmu Bobs", rada apakšaģentus, modernizē lieldatoru kodu, un piegādā analītikas produktu ar nosaukumu Bobalytics, tāpēc kaut kur kāda banka ir ļoti sajūsmā, un neviens nav lasījis licenci.

4:51 Tas ir daudz peļņas vienai piektdienai; ja vēlaties to lasīt, nevis dzirdēt mani sakām, "The Daily Diff" nonāk jūsu iesūtnē katru rītu – bez maksas vietnē thedailydiff.dev, saite zemāk. Tātad, šodienas spriedums: SHIP IT. Kodols saka jā, Buzzards saka jā, matemātika nav mainījusies, bet veids, kā mēs pārbaudām matemātiku, tikko mainījās. Tās ir šodienas izmaiņas. Esmu Niko no Axrisi.

5:09 Apvienojiet atbildīgi.

Avoti

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