Claude, Fermat'nın Son Teoremi'nin ilk eksiksiz bilgisayarla doğrulanmış Lean kanıtını yazdı

Anthropic makine doğrulamalı matematikte bir ilke imza attığını iddia ediyor

Anthropic, Fermat'nın Son Teoremi'nin (FLT) ilk eksiksiz, bilgisayarla doğrulanmış kanıtı olarak nitelendirdiği çalışmayı yayımladı. Şirkete göre Claude, kanıtı Lean proof assistant'ta yazmak için büyük ölçüde özerk biçimde 11 gün çalıştı; yaklaşık 13 milyon satırlık Lean kodu ve nihai argümanı oluşturan 29.500 ara teoremi üretti — matematikçilerin yıllar süreceğini öngördüğü bir formalizasyon.

Teoremin doğrulanması neden bu kadar zordu

FLT, 2'den büyük herhangi bir n için aⁿ + bⁿ = cⁿ denklemini sağlayan pozitif a, b ve c tam sayılarının bulunmadığını ifade eder. Anthropic'in anlattığına göre Fermat, bu iddiayı 1637 civarında Diophantus'un Arithmetica'esinin kendi nüshasının kenarına not düşmüş ve kenar boşluğunun kanıtını içerecek kadar geniş olmadığına dair ünlü sözünü de yanına eklemişti. 1908'de duyurulan bir ödül, yalnızca ilk yılında 621 hatalı girişim çekti.

Kabul gören ilk kanıtı Sir Andrew Wiles'ın yayımlamasından önce 350 yıldan fazla zaman geçti. Mayıs 1995'te yayımlanan kanıt 129 sayfaydı, Fermat'nın erişebileceğinin çok ötesinde modern tekniklere dayanıyordu ve zorlu bir incelemeden geçti: Wiles'ın 1993 konferanslarının doğrulanmasına başlanmasından iki ay sonra bir boşluk ortaya çıktı ve Wiles'ın bu boşluğu eski öğrencisi Richard Taylor ile kapatması yaklaşık bir yıl sürdü. Hollandalı bilgisayar bilimci Jan Bergstra daha sonra kanıtın makineyle doğrulanabilir bir forma dönüştürülmesini önerdi ve 2024'te Imperial College London'dan Kevin Buzzard, FLT'yi Lean'de formalize etmeye yönelik yıllar sürecek bir topluluk çabasını başlattı.

Claude kanıtı nasıl üretti

Anthropic'e göre, Columbia Üniversitesi'ndeki grubu yapay zekâ formalizasyon araçları geliştiren Anthropic araştırmacısı Tianyi Peng, Claude'un ne kadar ileri gidebileceğini test etmeye koyuldu ve sonuç beklentilerini aştı. Düzinelerce Claude agent'ı, kavramları tanımlamak, ara teoremleri kanıtlamak ve bunları daha güçlü ifadelerde birleştirmek için iş birliği yaparak Darmon, Diamond ve Taylor'ın basitleştirilmiş Wiles kanıtı versiyonunu izledi. İnsan katkısı, Peng'in bazı alt sonuçlara öncelik verilmesi gibi aralıklı üst düzey yönlendirmeleriyle sınırlıydı.

İlk denemeler başarısız oldu. Anthropic, agent'ların başlangıçta projenin durumunu takipten koptuğunu ve etkili iş birliğini bıraktığını söylüyor. Atılım, Peng ve Columbia'daki iş birlikçilerinin geliştirdiği açık iş birliği platformu Prove2Me ile geldi. Platform, agent'ların neyi deneyeceklerine karar vermek için kullandığı yönlü asiklik graf biçiminde teorem ifadelerini tutuyor, Lean derlemesini hızlandırmak için ifadeleri ve kanıtları ayrı dosyalara bölüyor ve agent'ların önceki çalışmaları arayıp yeniden kullanabilmesi için her teoremin doğal dil açıklamalarını saklıyor.

Son itki, Claude Code tabanlı bir çoklu agent harness'iyle yapıldı ve Anthropic'in kabaca Claude Fable 5.1 ile karşılaştırılabilir olarak nitelendirdiği genel amaçlı dahili bir araştırma modelinden yaklaşık altı milyar çıktı token'ı tüketti. Başarısız erken denemeler, bitmiş kanıttaki kalıp olmayan satırların yaklaşık %7'sine katkıda bulundu ve Claude yol boyunca toplam 30.300 teorem kanıtladı; bunların 29.500'ü nihai sürümde yer alıyor. Sonucu inceleyen Buzzard, bunu FLT'yi matematiğin aksiyomları ötesinde hiçbir varsayım olmaksızın kanıtlayan "olağanüstü bir otoformalizasyon başarısı" olarak nitelendirdi ve yapay zekâ formalizasyon çıktılarının artık üzerine inşa edilecek kadar sağlam olduğunu ekledi.

Yeni matematik değil, doğrulama

Anthropic, yeni matematik üreten yakın tarihli Riemann hipotezi çalışmalarının aksine burada teoremin çoktan kanıtlanmış olduğunu; ilerlemenin doğrulamanın kendisi olduğunu vurguluyor. Lean gibi proof assistant'lar mantığı algoritmik olarak doğrular, ancak darboğaz her zaman insan kanıtlarını — bariz adımları atlayan ve yüzyıllara yayılmış yayımlanmış çalışmalara dayanan — bir makinenin gerektirdiği tamamen açık forma yeniden yazmak olmuştur. Topluluğun yalnızca FLT formalizasyonunun ilk aşaması için kullandığı blueprint 86 sayfaya ulaşıyor. Claude'un bitmiş kanıtı, üzerine inşa edildiği formalize edilmiş matematiğin ana topluluk kütüphanesi Mathlib'in boyutunun beş katından fazla. Anthropic'in anlatımı zaman çizelgesini hem 11 günlük özerk çalışma hem de toplam çaba için iki haftanın biraz altı olarak veriyor.

Neden önemli

Bu ölçekte bir kanıtın formalizasyonu ucuz hale gelirse, matematiğe güvenmenin ekonomisi değişir. Derin sonuçların insanlar tarafından doğrulanması aylar veya yıllar sürebilirken, Lean ile doğrulanmış bir kanıt mekanik olarak onaylanır. Yapay zekâ sistemleri daha fazla matematiksel iddia ürettikçe, otoformalizasyon değerlendirme yükünün yönetilemez hale gelmesini önlemenin bir yolunu sunuyor. Anthropic umudu, matematiğin dayandığı bilgi birikimine güvenmenin zorlaşması değil kolaylaşması biçiminde çerçeveliyor. İki uyarıya değinmekte yarar var: işlem maliyeti — altı milyar çıktı token'ı — bunun hâlâ rutinden çok uzak olduğunu gösteriyor ve şu ana kadarki ayrıntılar, bağımsız bir değerlendirme yerine çalışmanın Anthropic'in kendi anlatımından geliyor.