Claude agentları Fermat'nın Son Teoremi'nin ilk bilgisayarla doğrulanmış Lean ispatını üretti

Ne oldu

4 Eylül'de Anthropic, duyurunun dev.to'daki yazısına göre, büyük ölçüde özerk çalışan bir Claude agent filosunun 11 gün sonunda Fermat'nın Son Teoremi'nin ilk eksiksiz, bilgisayarla doğrulanmış ispatını yayımladı. İspat, çekirdeği her mantıksal adımı doğrulayan bir proof assistant olan Lean dilinde yazıldı ve yaklaşık 350 yıl boyunca kanıtsız kalan bir önermeyi kapsıyor.

Fermat, varsayımını 1637 civarında bir kenara not etmişti: 2'den büyük hiçbir üs için aⁿ + bⁿ = cⁿ eşitliğini sağlayan pozitif a, b ve c tam sayıları yoktur. Andrew Wiles bunu 1995'te 129 sayfalık bir argümanla kanıtladı; 1993 sunumundaki bir boşluğu ortaya çıkaran bir hakemin sorusu sonrası bu boşluk, önce tek başına, sonra eski öğrencisi Richard Taylor ile birlikte bir yılda tamir edildi. Bu ispatın bir makine adım adım kontrol edebileceği biçimde yeniden yazılması, Londra'daki Imperial College'dan Kevin Buzzard öncülüğünde 2024'ten beri bir topluluk projesi. dev.to makalesine göre yalnızca ilk aşamanın planı 86 sayfa tutuyor ve çaba çok yıllı bir girişim olarak kapsamlandırılmıştı.

Columbia Üniversitesi'ndeki akademik grubu AI formalizasyon araçları geliştiren Anthropic araştırmacısı Tianyi Peng, Claude'un bu konuda ilerleyip ilerleyemeyeceğini test etmeye koyuldu. Anthropic'in kendi anlatımına göre sonuç, küçük ilerlemelerin çok ötesine gitti.

Çalışmanın ölçeği

Bildirildiğine göre çaba, 13 milyon satır Lean üretti; bu, üzerine inşa edildiği topluluk ispat kütüphanesi Mathlib'in boyutunun beş katından fazla, ancak Anthropic ispatın katı biçimde gerekenden daha uzun olduğunu belirtiyor. Agentlar 30.300 teorem kanıtladı (bunların 29.500'ü nihai ürüne besliyor) ve dahili bir araştırma modeliyle yaklaşık altı milyar çıktı token'i üretti. Düzineyle agent kavramlar tanımladı, ara sonuçlar kanıtladı ve bunları birbirine bağladı.

Önce gelen başarısızlık

dev.to yazarının öne çıkardığı ayrıntı, ilk denemelerin çökmesi. Anthropic'in gönderisine göre agentlar erken bir başarı yakaladı ama sonra projenin durumunu gözden kaybetti ve etkin işbirliğini kesti. Başarısız denemeler ile başarılı deneme arasında modelin kendisi değişmedi; koordinasyon katmanı değişti. Proje durumu, zamanla bozulan agent'ların context window'larında yaşıyordu; bu yüzden bir agent'ın zaten kanıtlanmış olanlara dair resmi bir diğerinkinden sapıyordu.

Çözüm, Peng ve Columbia'daki iş birlikçilerinin geliştirdiği açık bir platform olan Prove2Me oldu. Platform, agent'ların bundan sonra ne kanıtlayacaklarına karar verirken danıştığı, teorem önermelerinden oluşan yönlü asikliklik grafiğini korudu; teorem önermelerini ve ispatlarını ayrı dosyalarda tutarak Lean derlemesini hızlandırdı ve kaynak kullanımını azalttı; ayrıca sonraki agent'ların mevcut sonuçları yeniden türetmek yerine arayıp yeniden kullanabilmesi için her düğümün doğal dil açıklamasını sakladı. Başarısız denemeler boşa gitmedi: Anthropic, bunların nihai ispatın şablon olmayan satırlarının yaklaşık yüzde 7'sine katkı sağladığını söylüyor.

dev.to yazısı bunu, her düğümün net bir tamamlanma ölçütüne sahip bir teslimat olarak davrandığı, Make, Bazel ve CI pipeline'larının on yıllardır işi planlamasına benzer biçimde agent'lara teoremler için bir build system vermek olarak çerçeveliyor.

İnsan katkısı önceliklendirmeye indi. Peng'in kayıtlı yönlendirmeleri arasında "Jacobian'ın bir scheme olarak tanımlanması yüksek öncelikli görünüyor" ifadesi var. Agent'ların kendi logları bitiş çizgisini işaretliyor: "FLT kökü 18 Ağu 02:00:57Z'de prove2me üzerinde PROVED okunuyor."

Nasıl doğrulandı

Kimse 13 milyon satırı elle okumadı. Lean'in çekirdeği her adımı kontrol etti; ispat yalnızca Lean'in üç standart aksiyomuna dayanıyor ve atlanmış adım yok; ayrıca bir karşılaştırma aracı, nihai teorem önermesinin Mathlib'in kendi teorem önermesiyle eşleştiğini doğruladı. Buzzard sonucu inceled ve dev.to makalesine göre, FLT'nin otomatik formalizasyonu şu anda mümkünse matematikte otomasyona doğru önemli bir adım atılmış oldu yazdı.

Neden önemli

Bu, özerk AI araştırması için bir dönüm noktası: çok yıllı bir topluluk çalışması olarak kapsamlanan bir proje, tam da yüzyıllar boyunca dünyanın en iyi matematikçilerine direndiği için ünlü bir teoremde, 11 günlük büyük ölçüde gözetimsiz çalışmaya sıkıştırıldı.

Daha aktarılabilir ders başarısızlığa dair olan. Agent'lar işe en baştan muktedir görünüyordu; eksik olan paylaşılan bellekti. Proje durumu context window'lardan çıkıp her agent'ın okuyabileceği ve güvenebileceği bir bağımlılık grafiğine taşındığında aynı modeller başarılı oldu. Paylaşılan bir kod tabanına veya pipeline'a karşı birden çok agent çalıştıran herkes bu örüntüyü tanıyacaktır; çıkarım şu: dışsallaştırılmış durum bir tasarım kararıdır, model yeteneği değil.

Bu, mekanik doğrulamanın rolünü de vurguluyor. Bu ölçekte özerklik yalnızca Lean'in çekirdeği ve bir önerme karşılaştırıcısı çıktıyı kontrol edebildiği için savunulabilirdi; güven, agent'larda değil kapılarda. Bu arada insan katkısı ispat yazmaktan sıradaki önemli şeyi seçmeye kaydı.

Bir uyarı: buradaki rakamlar ve alıntılar tek bir ikincil yazı üzerinden aktarılan Anthropic'in kendi gönderisinden geliyor ve o yazı Buzzard'ın tam yorumuna ulaşmadan kesiliyor; dolayısıyla sonucun bağımsız değerlendirmesi hâlâ bekliyor.