Claude, Fermat’ın Son Teoremi’nin kanıtını makineye doğrulattı

Fermat’ın Son Teoremi tek cümleye sığıyor: n ikiden büyük bir tam sayıysa, hiçbir pozitif tam sayı üçlüsü x^n + y^n = z^n eşitliğini sağlayamaz.

n iki iken çözüm bol. Küplerde, dördüncü kuvvetlerde ve daha yukarısında ise tek bir tane bile yok, üstelik sonsuz sayıda denklemin hepsi için aynı anda.

Fermat bunu 1637’de Diophantus’un Arithmetica’sının kenar boşluğuna yazdı ve ekledi: gerçekten hayranlık verici bir kanıtını buldum, ama bu kenar onu almaz. O kanıt hiç ortaya çıkmadı.

Teorem 358 yıl açık kaldı. 1995’te Andrew Wiles kapattı, son boşluğu Richard Taylor ile birlikte doldurdu. Yani teoremi kanıtlayan Claude değil, Wiles.

Açık kalan başka bir şeydi: kanıtın, bir makinenin baştan sona denetleyebileceği bir biçimi yoktu. Bu ölçekteki bir kanıtı insanların satır satır denetlemesi yıllar alıyor.

Kevin Buzzard bu iş için 2024’te beş yıllık, 1 milyon sterlinlik bir hibe aldı. 2029 hedefi kanıtın tamamı bile değildi: teoremi, 1980’lerin sonunda bilinen bir dizi iddiaya indirgemekti.

Anthropic 4 Eylül’de duyurdu: Claude, Wiles’ın kanıtını Lean’e çevirdi ve baştan sona makineye doğrulattı. Ortaya çıkan şey, teoremin bilgisayarla denetlenmiş ilk kanıtı.

Çalışma ağustos başında başladı ve 11 gün sürdü. Claude bu süre boyunca büyük ölçüde kendi başına ilerledi. Kanıt 18 Ağustos’ta tamamlandı.

Yeni bir matematik üretilmedi. Değişen tek şey, kanıtın artık makinenin her satırını denetleyebildiği bir dilde durması.

Rakamlar alışılmış ölçeğin dışında.

Claude 13 milyon satır Lean kodu yazdı. Toplam 30.300 ara teorem kanıtladı, bunların 29.500’ünü nihai kanıtta kullandı. Üretilen çıktı yaklaşık 6 milyar token.

Karşılaştırma için: bu kod, Lean topluluğunun yıllar içinde kurduğu Mathlib kütüphanesinin beş katından büyük.

Bu iş tek bir modelin tek bir oturumu değildi. Claude Code üzerine çok ajanlı bir düzenek kuruldu ve düzinelerce ajan aynı anda çalıştı.

Ajanları bir arada tutan şey Prove2Me: Columbia Üniversitesi’nden Tianyi Peng ve ekibinin tasarladığı açık bir formalleştirme platformu. Teorem ifadelerini yönlü çevrimsiz bir grafikte tutuyor, Lean derlemesini hızlandırıyor ve kanıtlanmış teoremlerin doğal dille aranıp yeniden kullanılmasını sağlıyor.

Kullanılan model, Anthropic’in kabaca Claude Fable 5.1’e denk dediği bir iç araştırma modeli.

Sonuç boşlukta çıkmadı. Altında yıllardır süren üç topluluk projesi var: Mathlib, Kevin Buzzard’ın Imperial College London’daki FLT projesi ve flt-regular.

Claude bu çalışmalardan parçalar uyarladı. Bitmiş kanıtı Lean doğruladı; ayrı bir karşılaştırma aracı da kanıtlanan ifadenin Mathlib’deki teorem ifadesiyle aynı olduğunu gösterdi.

Buzzard’ın bu tarafa dair değerlendirmesi şöyle: “Bu olağanüstü otoformalleştirme başarısı, Fermat’ın Son Teoremi’ni matematiğin aksiyomları dışında hiçbir varsayım olmadan kanıtlıyor.”

Aynı Buzzard matematik tarafında çok daha sert: iş “kanıtın erken dönem literatürünü sadakatle takip ediyor ve hiçbir şey eklemiyor.” Yani matematiğe yeni bir bilgi girmiyor.

Kod 13,4 milyon satır ve 96 çekirdekli bir makinede derlenmesi neredeyse yirmi kat uzun sürüyor. Bu haliyle Mathlib’e de giremiyor: kütüphane yapay zekayla üretilmiş incelemeleri kabul etmiyor.

Geriye anlamsal bir boşluk kalıyor: ara ifadelerin, adlarının vaat ettiği matematiği gerçekten söyleyip söylemediğini hâlâ insanların denetlemesi gerekiyor.