Anthropic'un Claude agent'ları Fermat'nın Son Teoremi'nin makine denetimli Lean 4 kanıtını 11 günde üretti

Kanıt ve doğrulanma süreci

Fermat'nın Son Teoremi, 2'den büyük herhangi bir n tam sayısı için a üzeri n artı b üzeri n'in c üzeri n'e eşit olduğunu sağlayan pozitif a, b ve c tam sayılarının bulunmadığını söyler. Andrew Wiles'ın kanıtı, 1993 tarihli duyurusunda bir boşluk bulunmasının ardından Richard Taylor ile birlikte tamamlanmış ve Mayıs 1995'te 129 sayfa boyunca yayımlanmıştır. Bunun Lean içinde formalize edilmesi, argümanı o kadar ayrıntılı bir kod olarak yeniden yazmayı gerektirir ki proof assistant'ın kernel'i eksilen her adımı reddeder.

Depo güven tabanını açıkça ortaya koyuyor: tek satırlık bir teorem ifadesi ve kanıtın yalnızca Lean'in üç standart aksiyomuna — propext, Classical.choice ve Quot.sound — dayandığını, hiçbir sorry yer tutucusu ve kernel dışındaki derlenmiş koda kaçış sağlayan native_decide bulunmadığını gösteren bir derleme zamanı kontrolü.

dev.to raporu doğrulama sayılarını listeliyor: sıfırdan bir derleme 96 paralel iş üzerinde 5 saat 32 dakika sürdü ve 153 GB RAM'e kadar çıktı; karşılaştırıcı bir yeniden oynatma 230 GB ile 14 saat 46 dakika sürdü; bağımsız bir Rust Lean kernel implementasyonu olan nanoda, 1.052.234 bildirimi hatasız kontrol etti. Kod, Lean 4.33.1 altında 60.475 modüle yayılıyor. Okunabilirlik bilinçli olarak feda edildi: README, teorem adlarının makine tarafından üretildiğini ve artefaktın okunmak değil doğrulanmak üzere yazıldığını belirtiyor; bakımsız bir araştırma çıktısı olarak sunuluyor.

Agent'lar nasıl çalıştı

dev.to'nun aktardığına göre Anthropic'in araştırma yazısı, Columbia'dan Tianyi Peng tarafından geliştirilen Prove2Me platformunda Claude Code multi-agent bir yapı içinde çalışan düzinelerce Claude agent'ını kapsıyordu. Prove2Me, kökünde Fermat'nın Son Teoremi bulunan teorem ifadelerinden oluşan yönlendirilmiş asiklik bir graf tutuyor; böylece her agent hangi lemmaların kanıtlandığını ve hangilerinin hâlâ açık olduğunu görebiliyor. Model, kabaca Claude Fable 5.1 ile karşılaştırılabilir genel amaçlı bir iç araştırma modeli olarak tanımlanıyor.

Paylaşılan graf sonradan eklenen bir öğeydi. Erken denemeler, agent'lar projenin durumunu takibi kaybedip işbirliğini bıraktığı için çöktü; yine de bu girişimler boilerplate olmayan satırların yaklaşık yüzde 7'sine katkıda bulundu. İnsan katkısı, Peng'in ara sıra verdiği üst düzey yönlendirmelerle sınırlıydı. Agent'lar, Wiles ve Taylor–Wiles kanıtının 1995 tarihli Darmon–Diamond–Taylor sunumundan yararlandı. 11 gün sonra, 18 Ağustos'ta saat 02:00:57 UTC'de grafiğin kökü kanıtlanmış olarak işaretlendi.

dev.to'ya göre toplamda 29.500 ara teorem ve yaklaşık 6 milyar çıktı token'ı üretilerek kanıt, Lean'in standart matematik kütüphanesi Mathlib'in boyutunun beş katından büyük hale geldi.

Matematikçinin hükmü

Buzzard'ın kendi çabası 1 milyon sterlinlik, beş yıllık bir hibe taşıyor ve yalnızca planı 86 sayfaya ulaşıyor. Anthropic ona 500 GB RAM'li bir makine ödünç verdi; o da 13,4 milyondan fazla satırı kendisi derledi ve derlemenin, 96 çekirdekli bir makinede Mathlib'i derlemekten neredeyse 20 kat uzun sürdüğünü bildirdi. Hükmü iki yönlüydü: formalizasyon doğrulanıyor, ama matematiksel olarak "bize özünde hiçbir şey söylemiyor". Yazdığına göre teoremin doğru olduğuna zaten yüzde 99,9 emindi ve sayı teorisyenleri tamamen emindi; formal kanıt erken literatürü izliyor ve yeni bir matematik eklemiyor.

Onu heyecanlandıran şey ise otomatik formalizasyondaki — insan matematiğini makinece doğrulanabilir biçime dönüştürmedeki — ilerlemeydi. Sonuç ayrıca yaklaşık 20 yıllık bir liste olan Freek Wiedijk'ın formalizasyon zorluklarının sonuncusunu tamamlıyor. Maliyet konusunda Anthropic token sayılarını açıkladı ama dolar tutarını değil; David Jao dahil yorumcular, yaklaşık 6 milyar çıktı token'ını geçerli API fiyatlarıyla, model eğitimi hariç yaklaşık 300.000 dolara tahmin etti. Buzzard, kendisine beş yıllık fon verildiğini, Anthropic'in ise 11 günde bitirdiğini ironiyle belirtti; ama daha fazla para harcamış olabileceklerinden şüphelendi. Olayı ilk kez, Galler'deki Green Man festivalindeyken zayıf bağlantılı bir e-postayla duydu ve bilinmeyen göndereni başta bir deli olarak görüp ciddiye almadı.

Neden önemli

Hikaye sayı teorisinden çok makine tarafından üretilen artefaktların nasıl güven kazandığıyla ilgili. On üç milyon satır kabul edildi; çünkü tek satırlık bir ifadeye, üç standart aksiyona ve bağımsız şekilde implement edilmiş iki kernel'e dayanıyor — bu, küçük ve özenle incelenmiş bir spesifikasyonun, uygulamanın ona göre zorunlu kılan bir denetleyiciyle eşleşmesiyle aynı yapı.

Ayrıca multi-agent sistemlerdeki zor problemi izole ediyor: agent'lar, kanıtlanan ve açık kalan şeylerin açık bir grafiğini paylaşana kadar başarısız oldu. Denetleyicinin katı olduğu yerde, hiçbir insanın okumadığı makine yazımı kod yine de sağlam olabilir; olmadığı yerde ise aynı hacimdeki üretilmiş kod bir yük haline gelir.