Claude, Fermat'ın Son Teoremini 11 Günde Formalize Etti

Bir yapay zeka Fermat'ın Son Teoremini mi kanıtladı? Hayır. Andrew Wiles bunu 1995'te yaptı. Anthropic'in 4 Eylül'de duyurduğu şey farklı ve bize kalırsa daha ilginç: Claude, Wiles'ın kanıtını bilgisayarın satır satır denetleyebildiği Lean 4 koduna çevirdi. Matematikçiler bu işe "formalizasyon" diyor ve bu teorem için yıllar süreceğini düşünüyorlardı.

Ne yapıldı, tam olarak?

Anthropic'in araştırma yazısına göre çalışma, Claude Fable 5.1'e "kabaca denk" bir dahili araştırma modeliyle yürütüldü. Model 11 günde 13 milyon satır Lean kodu üretti, 30.300 ara teorem kanıtladı; bunların 29.500'ü nihai kanıtta kullanıldı. Sonuç Lean derleyicisinden geçti, yani her adım mekanik olarak doğrulandı. Imperial College London'dan Kevin Buzzard kanıtı inceledi ve teoremin ifadesinin Mathlib kütüphanesindeki sürümle eşleştiği ayrıca kontrol edildi.

Buzzard'ın yorumu ölçülü ama net: "Fermat'ın otomatik formalizasyonu bugün mümkünse, modern matematik literatürünün otomatik formalizasyonuna doğru büyük bir adım atmışız demektir."

11 gün ifadesi neyi gizliyor?

Takvimdeki 11 gün tek bir ajanın kesintisiz çalışması değil. Birkaç düzine ajan paralel koştu ve toplamda 6 milyar çıktı tokeni üretti. Bu kadar tokenin maliyeti açıklanmadı; kabaca hesaplarsanız bir KOBİ'nin yıllık yazılım bütçesini geçen bir rakam çıkar.

İlk deneme başarısız oldu. İş, Columbia Üniversitesi'nden Tianyi Peng'in ekibinin geliştirdiği Prove2Me adlı açık kaynaklı araç eklendikten sonra yürüdü; bu araç teoremler arasındaki bağımlılık grafiğini tutuyor ve ajanların hangi parçaya saldıracağını yönetiyor. Anthropic'in kendi notuna göre kodun boilerplate dışındaki satırlarının yaklaşık yüzde 7'si başarısız denemelerden kalma ve 13 milyon satırlık kanıt "muhtemelen gerekenden çok daha uzun".

Bir de temel var: çalışma, Buzzard'ın yıllardır yürüttüğü Imperial FLT projesinin ve Kummer teoremini formalize eden flt-regular projesinin üzerine kuruldu. Sıfırdan başlanmadı; insanların döşediği zemin olmadan bu sonuç çıkmazdı.

Peki neden önemli?

Çünkü bugüne kadar "yapay zeka matematik yapıyor" başlıklarının çoğu, doğruluğunu bir insanın kontrol etmesi gereken metin üretimiydi. Formalize edilmiş bir kanıtta kontrolü derleyici yapar; modelin ikna edici ama yanlış bir şey yazma ihtimali sıfıra iner. Bu, hakemli dergilerin yıllarca fark edemediği hataları yakalayabilecek bir araç demek. Anthropic bunu açıkça hedef olarak koyuyor: hakemlik yükünü azaltmak ve literatürdeki hataları ayıklamak.

Şüpheci tarafımız şunu da eklemeden duramıyor: 13 milyon satırlık bir kanıt, insanların okuyup öğrenebileceği bir şey değil. Doğru olduğunu biliyoruz; neden doğru olduğunu anlamayı yine insanlara bırakıyor.

Matematikçi olmayanlar için anlamı

Kimse Fermat için ajan kiralamayacak. Ama aynı mekanizma, yani "model üretsin, katı bir denetleyici doğrulasın, başarısızlar elensin" döngüsü, doğrulanabilir her işte çalışıyor: tip denetiminden geçen kod, testleri geçen yeniden yazımlar, şemaya uyan veri dönüşümleri. Türkiye'de bir yazılım ekibinin eski bir modülü 6 milyar token harcamadan yeniden yazması bugün mümkün, çünkü kural aynı: doğrulayıcı ne kadar sertse ajana o kadar güvenebilirsiniz. Denetleyicisi olmayan işlerde ise bu haber size hiçbir garanti vermiyor.

Kaynaklar: Anthropic: Formalizing Fermat's Last Theorem, GitHub: kanıt deposu, SiliconANGLE