Lean ile Fermat'nın Son Teoremi: Çok Ajanlı Kodlama İçin Dersler

Anthropic 4 Eylül'de Formalizing Fermat's Last Theorem başlıklı yazıyı yayımladı. Yazı, teoremin uçtan uca, bilgisayarla denetlenmiş ve Lean'de doğrulanmış ilk ispatını anlatıyor. İspatı bir grup Claude ajanı 11 günde, büyük ölçüde otonom olarak üretti. Ajanlar Claude Code tabanlı çok ajanlı bir harness üzerinde ve yazının kabaca Claude Fable 5.1 ile karşılaştırılabilir dediği şirket içi bir araştırma modeliyle çalıştı. Matematiği değerlendirecek durumda değilim. Mühendisliği ise değerlendirebilirim, çünkü bu kurulum her gün yaptığım işin büyütülmüş hâli: tek bir kod tabanında çalışan birkaç kodlama ajanı ve neyin "bitti" sayılacağına karar veren bir makine.

Gerçekte ne teslim edildi#

Yazıya ve açık kaynak repoya göre:

• Yaklaşık 13 milyon satır Lean. Bu, topluluğun ana matematik kütüphanesi Mathlib'in 5 katından fazla.
• İspatlanan 30.300 teorem. Bunların 29.500'ü nihai ispatta kullanılıyor.
• Kabaca 6 milyar çıktı token'ı.
• Mathlib v4.33.0 üzerinde Lean 4.33.1, Apache 2.0 lisanslı. Yalnızca Lean'in üç standart aksiyomuna dayanıyor, hiç sorry ya da native_decide yok.

Lean çekirdeğinin her tanımı denetlediği build'in kendisinin yanında iki kontrol daha çalıştırıldı. Birincisi, önermeyi yalnızca Mathlib kullanılarak yazılmış bir önermeyle karşılaştıran ve ispatı çekirdekten yeniden geçiren bir karşılaştırıcı (comparator). İkincisi, 1.052.234 tanımı denetleyen bağımsız bir Rust çekirdeği olan nanoda.

İşin asıl faydalı kısmı ilk başarısızlık#

İlk denemeler başarısız oldu, çünkü ajanlar "projenin durumunu kısa sürede kaybetti ve etkili biçimde iş birliği yapmayı bıraktı." Yazının anlattığı çözüm daha iyi bir model değildi. Çözüm ortak durumdu (shared state).

Bu çözüm, Columbia'dan Tianyi Peng ve ekibinin geliştirdiği açık bir formalizasyon platformu olan Prove2Me oldu. Prove2Me:

• Teorem önermelerinden oluşan yönlü, döngüsüz bir grafik (DAG) tuttu. Ajanlar sıradaki ispatı bu grafiğe bakarak seçti.
• Önermeleri ve ispatları ayrı dosyalarda sakladı, aralarındaki bağlantıları bağımsız olarak tuttu. Bu da derlemeyi hızlandırdı.
• Her önermenin doğal dildeki bir açıklamasını tuttu. Böylece ajanlar mevcut sonuçları arayıp yeniden kullanabildi.

Yazıya göre DAG, bellek bozulmasına (memory degradation) karşı işe yaradı ve birden fazla ajanın paralel çalışmasını sağladı. Paralel kodlama ajanları da daha küçük ölçekte aynı şekilde başarısız oluyor. Kod yazamadıkları için değil; ikisi aynı yardımcı fonksiyonu baştan yazdığı ya da biri neyin bittiğine dair eskimiş bir resimle çalıştığı için.

Pazarlık etmeyen bir denetleyici#

Üretilmiş 13 milyon satırı değerli kılan şey Lean. Bir ispat ya derlenir ya derlenmez, kimseyi ikna etmeye gerek yok. Repo sınırı da açıkça belirtiyor: Ara bir teoremin, adının ima ettiği şeyi gerçekten ifade edip etmediğini hiçbir araç denetlemiyor.

Yazılımda bunun daha zayıf versiyonları var: tip denetleyicisi, contract testleri, şema doğrulama, merge'ü engelleyen CI. Ajanları, gün sonunda bir diff'e göz gezdiren bir insana göre değil, bu kapılara (gate) göre değerlendirin. Geliştirdiğim review CLI'ı Quorate da aynı içgüdüyle çalışıyor: önce birkaç AI reviewer, ardından deterministik bir PASS/WARN/FAIL kapısı. FLT reposu bir adım daha ileri gidiyor: #guard_msgs, #print axioms'u sarmalıyor; böylece ispat üç standart aksiyomun ötesinde herhangi bir şeye dayanırsa build kırılıyor. Yazılımdaki karşılığı, kritik bir yola biri @ts-ignore, atlanmış bir test ya da yeni bir any eklediğinde kırılan bir CI adımı.

Önce kontratlar, sonra implementasyonlar#

Önermeleri ispatlardan ayırmak, olduğu gibi kopyalayacağım kısım. Repoda Theorems/ önermeleri, P2M/Sol/ ispatları, Definitions/ ise tanımları tutuyor ve her ispat, atıfta bulunduğu önermeleri import ediyor. Önerme kontratın ta kendisi. Onu sağlayan her ispat kabul edilebilir.

Bir kod tabanında bu şu anlama geliyor: Interface'ler, API şemaları ve tipli imzalar önce, kendi başlarına bir birim olarak review ediliyor; implementasyonlar ancak sonra ajanlara dağıtılıyor. Doğal dildeki indeks ise çoğu ekipte eksik olan bir şeye karşılık geliyor: her modülün halihazırda ne yaptığının aranabilir bir açıklaması. Böylece bir ajan dördüncü tarih parser'ını yazmadan önce mevcut olanı buluyor. Yeniden kullanım dışarıya doğru da işledi: İspat, Kevin Buzzard'ın Imperial College London'daki FLT projesinden ve flt-regular'dan parçalar uyarlıyor.

Pazartesi neye bakardım#

• Görev durumu açık mı? Ajanların okuyup güncellediği bir bağımlılık grafiği ya da görev dosyası olmalı; durum her ajanın kendi context'inde yaşamamalı.
• Kontratlar ayrı review ediliyor mu? Interface ve şema değişiklikleri, implementasyon PR'larından önce kendi review'larından geçmeli.
• Kapınız hiçbir şeye güvenmiyor mu? Tek kontrolünüz "başka bir model de baktı" ise, bir kapınız yok demektir.
• Ajanlar var olanı bulabiliyor mu? Bakımı yapılan bir modül indeksi, retrieval'ın şansının yaver gitmesini ummaktan iyidir.

Benim yorumum#

Yazı maliyetler konusunda açık sözlü. İspat "muhtemelen olması gerekenden çok daha uzun", proje yoğun token tüketti, başarısız denemeler hâlâ boilerplate dışı satırların yaklaşık %7'sini oluşturuyor ve repo, isimlerin makine tarafından üretildiğini, asıl önemli olanın önermeler olduğunu belirtiyor. Bir ürün kod tabanındaki ajan çıktısı da buna benziyor: denetleyiciye göre doğru, uzun soluklu, bakımı zor. Resmi bir ispat bunu kaldırabilir, çünkü reponun ifadesiyle okunmak için değil denetlenmek için yazılıyor. Çoğu yazılım bunu kaldıramaz.

Dolayısıyla bu bana backlog'u bir ajan sürüsüne devretmemi söylemiyor. Ajan eklemeden önce nereye yatırım yapmam gerektiğini söylüyor: ortak durum, kontratlar ve lafla ikna edilemeyen bir denetleyici. Anthropic ayrıca üç kişisel Claude Max planı üzerinde çalışan ajanların, Prove2Me aracılığıyla Vinogradov'un Üç Asal Teoremi'ni üç günde formalize ettiğini aktarıyor ve doğru iskeletle (scaffold) bu tür işlerin tüketici abonelikleriyle bile yapılabilir hâle geldiğini savunuyor. Bence aynısı yazılım ekipleri için de geçerli.