Claude membuktikan Fermat dalam 11 hari. Keputusan: SHIP IT.

Apa yang diliputi video ini

• Claude memformalkan Teorem Terakhir Fermat dalam Lean 4
• RCE kotak pasir Chromium (CVE-2026-85046), dieksploitasi dalam alam liar, ganjaran $1,000
• Shin Jin-seo mengalahkan KataGo dengan handicap dua batu

Transkrip terjemahan

Diterjemahkan daripada penceritaan asal Bahasa Inggeris. Audio dan kapsyen yang tersedia dikawal oleh YouTube.

0:00 Fermat berkata buktinya yang menakjubkan tidak akan muat di pinggir, dan hari ini Anthropic menerbitkan pinggirnya: tiga belas juta baris Lean, lima kali saiz Mathlib, membuktikan teorem yang sudah dipercayai oleh setiap ahli matematik. Ia adalah antara pukul sepuluh dan sebelas di Tbilisi ketika Anthropic membuat siaran, jadi secara semula jadi saya terjaga. Semalam Google melancarkan Chrome 152 dengan dua belas pembetulan keselamatan, salah satunya adalah pepijat V8 yang sudah dieksploitasi dalam alam liar, dan membayar pelapor seribu dolar, yang kurang daripada sedan yang akan kita bincangkan kemudian.

0:26 Juga semalam, Mullvad berkata ia akan menutup DNS awam yang dienkripsikan pada 2 November dan membayar Quad9 untuk melakukannya, dan pagi ini Rust React Compiler menjadi asli dalam Vite, sementara Hacker News menemui IBM Bob, ejen pengekodan AI. Kemudian Claude memformalkan Teorem Terakhir Fermat, dan di halaman depan yang sama seorang grandmaster Korea mengalahkan enjin Go terkuat di Bumi, jadi hari ini manusia menang satu daripada dua. Dalam video ini: apa yang Claude sebenarnya buktikan, berapa kosnya,

0:52 mengapa ahli matematik yang menghabiskan kerjayanya untuk ini mengatakan ia tidak mengubah apa-apa dan tetap gembira, dan bagaimana manusia mengalahkan mesin dalam Go. Hari ini Jumaat, 4 September, dan ini adalah The Daily Diff. Teorem Terakhir Fermat: tiada integer positif a, b, c memuaskan a kuasa n tambah b kuasa n sama dengan c kuasa n untuk sebarang n di atas 2. Fermat mencatatkannya di pinggir sekitar tahun 1637 dan meninggal tanpa menunjukkan karyanya, menjadikannya pembangun pertama yang menutup tiket dengan berfungsi pada mesin saya. Hadiah 100,000 mark emas pada tahun 1908 menarik 621 bukti

1:25 yang salah pada tahun pertamanya, dan Andrew Wiles akhirnya mendapatkannya pada tahun 1995, dalam 129 halaman yang memerlukan pengadil berbulan-bulan untuk mengesahkan. Formalisasi bermaksud menulis semula bukti itu supaya Lean, pembantu bukti, dapat memeriksa setiap langkah secara mekanikal, dan Kevin Buzzard di Imperial telah memimpin usaha manusia untuk melakukan perkara itu sejak tahun 2024; pelan tindakan sahaja berjumlah 86 halaman. Penyelidik Anthropic Tianyi Peng menunjuk berpuluh-puluh ejen Claude kepadanya sebaliknya, di platform bernama Prove2Me yang menyimpan DAG pernyataan teorem supaya ejen tahu apa yang perlu dibuktikan seterusnya, kerana tanpanya gerombolan

2:00 pertama kehilangan jejak siapa yang membuktikan apa, itulah yang berlaku apabila lapisan orkestrasi anda adalah regex dengan bajet pemasaran. Sebelas hari kemudian nod akar berbunyi DIBUKTIKAN: tiga belas juta baris Lean, 29,500 teorem perantaraan, kira-kira enam bilion token output dari model dalaman yang secara kasar setanding dengan Claude Fable 5.1. Binaan gagal melainkan bukti itu berdasarkan tepat tiga aksiom piawai Lean: tiada maaf, tiada keputusan asli, tiada penipuan. Memeriksanya juga tidak murah: binaan dari

2:29 awal mengambil masa lima setengah jam pada 96 teras dan 153 gigabait RAM, dan nama-nama teorem adalah dijana mesin, jadi repositori itu menggambarkan dirinya ditulis untuk diperiksa daripada dibaca, yang juga bagaimana saya akan menggambarkan Java perusahaan. Sekarang percanggahan itu. Catatan Anthropic mengatakan Lean menunjukkan kebetulan tanpa keraguan. Kevin Buzzard, lelaki yang dikalahkan, mengkompilasi repositori pada mesin 500-gigabait yang dipinjamkan oleh Anthropic kepadanya, mengesahkan ia diperiksa, dan kemudian menulis,

2:56 petikan, secara matematik kerja ini tidak memberitahu kita apa-apa. Dia sudah 99.9 peratus yakin teorem itu benar, dan bukti itu tidak menambah matematik baru; apa yang ditunjukkannya ialah apa yang boleh dilakukan oleh autoformalisasi sekarang, dan bahagian itu dia benar-benar teruja mengenainya. Dia diberi satu juta paun selama lima tahun; Anthropic mengambil masa sebelas hari, dan pengiraan kasar seorang pengulas meletakkan enam bilion token output pada harga senarai sekitar 300,000 dolar, jadi mesin itu lebih murah, melainkan jika anda mengira melatih mesin, yang tiada siapa buat.

3:24 Butiran terbaik: e-mel itu tiba semasa dia berada di festival muzik di Wales dengan satu bar 4G, daripada nama yang tidak pernah didengarnya, jadi dia menganggapnya sebagai gurauan dan membacanya seminggu kemudian, yang merupakan respons yang betul kepada mana-mana baris subjek mengandungi formalisasi hujung-ke-hujung. Sementara itu, manusia mendapat satu kembali. Shin Jin-seo, pemain nombor satu dunia dalam Go, mengalahkan KataGo, enjin Go sumber terbuka terkuat, dua permainan berbanding satu di Seoul dengan dua-batu handicap, kira-kira jurang antara profesional terkemuka dan profesional baru.

3:50 Penentu adalah kemenangan 11.5 mata dalam 221 langkah, memegang 99 peratus kebarangkalian kemenangan dari pertengahan permainan, dan dia membawa pulang 250 juta won, kira-kira 170,000 dolar, ditambah Genesis G90, jadi ganjaran untuk mengalahkan AI super-manusia adalah 170 kali ganjaran Google untuk kotak pasir Chrome melarikan diri. Penjelasannya: pada awalnya dia menyalin langkah-langkah AI dan kalah; dia menang dengan membina papan dalam gayanya sendiri, yang merupakan nasihat paling berguna tentang AI yang saya dengar sepanjang tahun ini, dan ia datang dari permainan papan. Dua baris lagi dalam diff.

4:22 Penyusun Rust React dari oxc kini asli dalam Vite di belakang satu bendera; sebuah kod asas 1,036 fail berubah dari 14.3 saat menjadi 0.81 dalam langkah kompilasi, kebanyakannya dengan memadamkan Babel daripada package.json, yang juga rutin penjagaan kulit saya. Dan IBM melancarkan Bob, rakan kongsi pengekodan AI yang menyambut anda dengan Hai, Saya Bob, melahirkan sub-ejen, memodenkan kod kerangka utama, dan menghantar produk analitik bernama Bobalytics, jadi di suatu tempat bank sangat teruja dan tiada siapa yang membaca lesen itu.

4:51 Itu banyak margin untuk satu Jumaat; jika anda lebih suka membaca ini daripada mendengar saya mengatakannya, diff tiba di peti masuk anda setiap pagi — percuma di the daily diff dot dev, pautan di bawah. Jadi, keputusan hari ini: SHIP IT. Kernel berkata ya, Buzzard berkata ya, matematik tidak berubah, tetapi cara kita memeriksa matematik baru sahaja berubah. Itulah diff hari ini. Saya Niko dari Axrisi.

5:09 Gabungkan dengan bertanggungjawab.

Sumber

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