Claude 11 günde Fermat'ı kanıtladı. Karar: SHIP IT.

Bu video neleri kapsar

• Claude, Fermat'ın Son Teoremi'ni Lean 4'te resmileştiriyor
• Chromium sanal alan RCE (CVE-2026-85046), gerçek hayatta istismar edildi, 1.000 dolar ödül
• Shin Jin-seo, KataGo'yu iki taş handikapla yendi

Çevrilmiş deşifre

Orijinal İngilizce anlatımdan çevrilmiştir. Mevcut ses ve altyazılar YouTube tarafından kontrol edilir.

0:00 Fermat, muhteşem kanıtının kenar boşluğuna sığmayacağını söylemişti, ve bugün Anthropic, kenar boşluğunu yayınladı: on üç milyon satır Lean, Mathlib'in beş katı büyüklüğünde, her matematikçinin zaten inandığı bir teoremi kanıtlıyor. Anthropic gönderdiğinde Tiflis'te onda on bir bu yüzden doğal olarak uyanıktım. Dün Google, on iki güvenlik düzeltmesiyle Chrome 152'yi yayınladı, bunlardan biri zaten gerçek hayatta istismar edilmiş bir V8 hatasıydı ve muhabire bin dolar ödedi, ki bu daha sonra değineceğimiz sedandan daha az.

0:26 Dün ayrıca Mullvad, herkese açık şifreli DNS'ini 2 Kasım'da kapatacağını ve bunun yerine Quad9'a ödeme yapacağını söyledi, bu sabah ise Rust React Derleyici Vite'de yerel hale geldi, Hacker News ise IBM Bob'u keşfetti, bir yapay zeka kodlama aracısı. Sonra Claude, Fermat'ın Son Teoremi'ni resmileştirdi ve aynı ön sayfada bir Koreli büyük usta, dünyadaki en güçlü Go motorunu yendi, bu yüzden bugün insanlık ikide bir yaptı. Bu videoda: Claude'un aslında neyi kanıtladığı, maliyeti,

0:52 kariyerini buna adamış matematikçinin neden hiçbir şeyi değiştirmediğini ve yine de heyecanlı olduğunu, ve bir insanın Go'da makineyi nasıl yendiğini. Bugün 4 Eylül Cuma ve bu The Daily Diff. Fermat'ın Son Teoremi: hiçbir pozitif tam sayı a, b, c 2'nin üzerindeki herhangi bir n için a üssü n artı b üssü n eşittir c üssü n eşitliğini sağlamaz. Fermat bunu yaklaşık 1637'de bir kenar boşluğuna karaladı ve çalışmasını göstermeden öldü, bunu makinemde çalışıyor diyerek bir bileti kapatan ilk geliştirici yaptı. 1908'de 100.000 altın marklık bir ödül, ilk yılında 621 yanlış

1:25 kanıt çekti ve Andrew Wiles sonunda bunu 1995'te başardı, hakemlerin doğrulaması aylar süren 129 sayfalık bir çalışmayla. Resmileştirme, bu kanıtı Lean'in, bir kanıt yardımcısının, her adımı mekanik olarak kontrol edebilmesi için yeniden yazmak demektir ve Imperial'dan Kevin Buzzard, 2024'ten beri tam da bunu yapmak için insani bir çabaya liderlik etmektedir; sadece taslağı 86 sayfa tutmaktadır. Anthropic araştırmacısı Tianyi Peng, bunun yerine onlarca Claude ajanını Prove2Me adlı bir platforma yönlendirdi, bu platform bir teorem ifadelerinin DAG'ını tutar, böylece ajanlar bir sonraki neyi kanıtlayacaklarını bilirler, çünkü bu olmadan ilk

2:00 sürüler kimin neyi kanıtladığının izini kaybetti, bu da orkestrasyon katmanınızın pazarlama bütçesi olan regex olduğu zaman olur. orkestrasyon katmanınız pazarlama bütçeli regex olduğunda olan şeydir. On bir gün sonra kök düğüm KANITLANDI yazıyordu: on üç milyon satır Lean, 29.500 ara teorem, yaklaşık altı milyar çıktı tokeni Claude Fable 5.1 ile kabaca karşılaştırılabilir dahili bir modelden. Kanıt, tam olarak Lean'in üç standart aksiyomuna dayanmadıkça derleme başarısız olur: hayır üzgünüm, yerel karar yok, hile yok. Kontrol etmek de ucuz değil: sıfırdan bir

2:29 derleme doksan altı çekirdekte ve 153 gigabayt RAM'de beş buçuk saat sürdü ve teorem adları makine tarafından oluşturuldu, bu yüzden repo kendini okunmak yerine kontrol edilmek üzere yazılmış olarak tanımlıyor, ki kurumsal Java'yı da böyle tanımlardım. Şimdi çelişki. Anthropic'in gönderisi, Lean'in doğruluğu şüphesiz bir şekilde gösterdiğini söylüyor. Bunu başarmakta yenilen Kevin Buzzard, Anthropic'in kendisine ödünç verdiği 500 gigabaytlık bir makinede repoyu derledi, kontrol ettiğini doğruladı ve sonra şunu yazdı, alıntı:

2:56 Matematiksel olarak bu çalışma bize esasen hiçbir şey söylemiyor. Teoremin doğru olduğundan zaten yüzde 99,9 emindi, ve kanıt yeni bir matematik eklemiyor; gösterdiği şey, otomatik formalizasyonun artık yapabildikleridir ve bu kısmından gerçekten heyecan duyuyor. Beş yıl boyunca bir milyon pound verildi; Anthropic on bir gün sürdü, ve bir yorumcunun kaba hesabı, altı milyar çıktı tokeninin liste fiyatını belirtiyor. yaklaşık 300.000 dolar, yani makine daha ucuzdu, makineyi eğitmeyi saymazsanız, ki kimse saymaz.

3:24 En iyi ayrıntı: E-posta, Galler'deki bir müzik festivalindeyken, kendisiyle birlikteyken geldi, bir çubuk 4G ile, hiç duymadığı bir isimden, bu yüzden onu bir şaka olarak görmezden geldi ve bir hafta sonra okudu, bu da herhangi bir konu başlığına verilen doğru tepkidir uçtan uca resmileştirme içeren. Bu arada, insanlar bir geri dönüş yaptı. Go'da dünya bir numarası olan Shin Jin-seo, KataGo'yu yendi, en güçlü açık kaynaklı Go motoru, Seul'de iki taşa karşı iki oyun bir handikap, kabaca üst düzey bir profesyonel ile acemi bir profesyonel arasındaki fark.

3:50 Belirleyici, 221 hamlede 11.5 puanlık bir galibiyetti ve orta oyundan itibaren yüzde 99 kazanma olasılığını koruyarak, 250 milyon kazandı won, yaklaşık 170.000 dolar, artı bir Genesis G90, yani süper insan bir yapay zekayı yenmenin ödülü Google'ın Chrome sandbox kaçışı için verdiği ödülden 170 kat fazla. Açıklaması: başlarda yapay zeka hamlelerini kopyaladı ve kaybetti; kendi tarzında tahtayı kurarak kazandı, ki bu, bu yıl yapay zeka hakkında duyduğum en faydalı tavsiye ve bir masa oyunundan geldi. ki bu, bu yıl yapay zeka hakkında duyduğum en faydalı tavsiye ve bir masa oyunundan geldi. ki bu, bu yıl yapay zeka hakkında duyduğum en faydalı tavsiye ve bir masa oyunundan geldi. Farkta iki satır daha.

4:22 Oxc'den Rust React Compiler artık Vite'de tek bir bayrağın arkasında yerel; 1.036 dosyalı bir kod tabanı derleme adımında 14.3 saniyeden 0.81 saniyeye düştü, çoğunlukla package.json'dan Babel'i silerek, ki bu da benim cilt bakımı rutinim. package.json'dan Babel'i silerek, ki bu da benim cilt bakımı rutinim. Ve IBM, sizi 'Merhaba, Ben Bob' diyerek karşılayan bir yapay zeka kodlama ortağı olan Bob'u piyasaya sürdü. Ben Bob, alt aracıları türetiyor, ana bilgisayar kodunu modernize ediyor, ve Bobalytics adında bir analiz ürünü gönderiyor, bu yüzden bir yerlerde bir banka çok heyecanlı ve kimse lisansı okumadı.

4:51 Bir cuma günü için bu çok fazla kar marjı; eğer bunu duymak yerine okumayı tercih ederseniz, fark her sabah gelen kutunuza düşer — daily diff dot dev'de ücretsiz, bağlantı aşağıda. dev, bağlantı aşağıda. Yani, bugünün kararı: SHIP IT. Çekirdek evet diyor, Buzzard evet diyor, matematik değişmedi, ama matematiği kontrol etme şeklimiz az önce değişti. İşte bugünün farkı. Ben Axrisi'den Niko.

5:09 Sorumlu bir şekilde birleştirin.

Kaynaklar

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