Anthropic’in Fermat’nın Son Teoremi Lean İspatı: Nasıl Doğrulanır?

“Claude, Fermat’nın Son Teoremi’ni çözdü” başlığını gördüğünüzde kritik kelimeye dikkat edin: biçimselleştirdi. Anthropic, teoremi baştan sona kontrol ettiğini söylediği herkese açık bir Lean çıktısı yayımladı. Ancak kullanılan matematiksel yol yeni keşfedilmiş bir ispat değil; Frey–Serre–Ribet–Wiles–Taylor-Wiles çizgisindeki yerleşik yaklaşım.

Önce iki farklı iddiayı birbirinden ayırın

Dar anlamıyla cevap evet: Anthropic, Fermat’nın Son Teoremi’nin (FLT) Lean 4 biçimselleştirmesini içeren, derleme ve doğrulama talimatları sunan herkese açık bir depo yayımladı. Fakat Claude’un bu ünlü problemi bağımsız biçimde çözdüğü iddiası doğru değil; matematiksel atılımı onlarca yıl önce Andrew Wiles ve Richard Taylor gerçekleştirdi.

FLT, n > 2 olduğunda a^n + b^n = c^n denkleminin pozitif tam sayılarda çözümü olmadığını söyler. Wiles’ın ispatı 1995’te yayımlandı; Anthropic’in çalışması ise bu yerleşik yaklaşımı makine tarafından denetlenebilir bir çıktıya dönüştürüyor. Tarihsel arka plan için Lean Community’nin FLT proje duyurusuna bakabilirsiniz.

Lean ispatı, gayriresmî bir matematik makalesinden farklı bir soruya yanıt verir. Belirli bir ortamda, kesin biçimde kodlanmış bir önermenin denetlenmiş tanım, bağımlılık ve aksiyomlardan türetilebildiğini gösterebilir. Ancak altta yatan matematiği bir yapay zekânın icat ettiğini ya da teorem adlarının açıklamalarıyla örtüştüğünü kanıtlamaz.

Anthropic gerçekte ne yayımladı?

Anthropic’in 4 Eylül 2026 tarihli araştırma yazısında, Claude’un FLT’nin ilk eksiksiz ve baştan sona bilgisayar tarafından denetlenmiş Lean biçimselleştirmesini 11 günde ürettiği belirtiliyor. Yazıya göre çalışmada yaklaşık 13 milyon satır Lean kodu, kanıtlanmış 30.300 teorem önermesi ve nihai ispatta kullanılan 29.500 önerme bulunuyor. Ayrıca yaklaşık 6 milyar çıktı token’ından söz ediliyor.

Çalışmada Prove2Me kullanıldı. Anthropic bu platformu, teorem önermelerinden oluşan yönlendirilmiş döngüsüz bir grafiği yöneten ve birden fazla aracıyı koordine eden bir sistem olarak tanımlıyor. Anthropic’e göre biçimselleştirme, Frey, Serre, Ribet, Wiles ve Taylor-Wiles’la ilişkilendirilen yerleşik ispat yolunun sadeleştirilmiş bir anlatımını izliyor.

İddiayı kontrol etmek için herkese açık GitHub deposu, duyurudan daha kullanışlı. Varsayılan hedef FinalCheck.lean dosyası ve teorem bildirimi şöyle:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
  (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
  a ^ n + b ^ n ≠ c ^ n

Depo, kendisini bakımı yapılmayan ve katkı kabul etmeyen bir araştırma çıktısı olarak tanımlıyor. Lean 4.33.1 ile Mathlib v4.33.0 sürümlerini sabitliyor; PROOF-PATH.md dosyasını içeriyor ve teorem ile tanım grafiğinin internet tarayıcısından çevrimdışı incelenebilmesini sağlayan bir HTML çıktısı sunuyor.

Deponun son kontrolü; ispatın eklenmiş bir aksiyoma, sorry ifadesine, native_decide, unsafe ya da benzer bir kaçış mekanizmasına dayanması hâlinde başarısız olacak şekilde tasarlanmış. Böylece okuyuculardan bir ekran görüntüsüne veya açıklama metnine güvenmeleri istenmiyor; çıktı doğrudan incelenebiliyor.

Tekrarlanabilir doğrulama yolu

Sağlıklı bir kontrol, izole bir .lean dosyasını farklı bir projeye kopyalamakla değil, deponun sabitlediği ortamı kullanmakla başlar. Lean Community’nin doğrulama rehberi bunun nedenini açıklıyor: Lean her ay sürüm yayımlıyor, Mathlib sık sık değişiyor ve geriye dönük uyumluluk garanti edilmiyor.

Derlemeden önce ortamı sabitleyin

Depoya göre derleme Linux veya macOS üzerinde yapılmalı. Bunun için elan, Git, Python, GNU coreutils ve Lake’in sabitlenmiş bağımlılıkları indirip derleyebilmesi için internet bağlantısı gerekiyor. Depo, .lake altında yaklaşık 67 GB alan ve sonradan silinebilecek yaklaşık 220 GB oluşturulmuş C dosyası gerektiğini belirtiyor.

Depo ayrıca her paralel iş için yaklaşık 5 GB bellek gerektiğini, bazı modüllerin ise 36 GB’a kadar çıkabildiğini bildiriyor. 96 iş parçacığıyla yapılan kendi derlemesi 5 saat 32 dakika sürmüş ve bellek kullanımı 153 GB ile zirveye ulaşmış. Bunlar bu makalede ölçülmüş sonuçlar değil, deponun paylaştığı rakamlar; kesin çalışma süresi olarak değil, donanım planlaması için bir uyarı olarak değerlendirin.

Doğrulama yöntemini seçin

• Sadece inceleme: Derleme yapmadan FinalCheck.lean, PROOF-PATH.md ve ATTRIBUTION.md dosyalarını okuyun.
• Tam Lean derlemesi: Sabitlenmiş araç zincirini kullanıp lake build komutunu çalıştırın.
• Bağımsız yeniden oynatma: Derleme ve dışa aktarma başarılı olduktan sonra karşılaştırıcı ile nanoda betiklerini çalıştırın.

Yeni klonlanmış bir depoda önerilen genel sıra şöyle:

git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt

# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build

# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh

# Run after the comparator check.
verification/nanoda/run.sh

Her aşamanın amacı farklı:

Karşılaştırıcı, teorem bildirimini okumaya alternatif değil. Bir projenin daha zayıf ya da ince bir farkla değiştirilmiş bir önermeyi kanıtlamış olabileceği riskini azaltmaya yardımcı oluyor. Deponun PROOF-PATH.md dosyası, matematiksel adımları Lean bildirimleriyle eşleştiriyor. Oluşturulan HTML sayfaları da bir web uygulaması çalıştırmadan bağımlılıkları incelemenizi sağlıyor.

Depo, ikinci kontroller için ek kaynak gereksinimleri de bildiriyor: 37,8 GB’lık dışa aktarım dosyasını yazmak yaklaşık 90 GB bellek isteyebilir; nanoda iş akışı sırasında ise yaklaşık 40 GB bellek gerekebilir.

Kanıtın gösterdikleri ve gösteremedikleri

Lean Community’nin “Did you prove it?” kontrol listesi temel kuralı net biçimde ortaya koyuyor: derleme, kodlanmış önermeyi doğrular; teorem adının hedeflenen gayriresmî iddiayla örtüşüp örtüşmediğini değil. Bu çıktıda karşılaştırıcı ve Mathlib kullanımı riski azaltıyor, ancak yine de teorem bildirimini ve ispat yolunu okuma gereğini ortadan kaldırmıyor.

Bu çıktı neyi gösteriyor, neyi göstermiyor?

Sistem, alışılmadık ölçekte biçimsel olarak denetlenmiş bir Lean çıktısı üretti. Ancak bu çalışma FLT için yeni bir yol, yeni bir elementer ispat veya Claude’un bağımsız matematiksel keşfini göstermiyor.

Anthropic, ispatın Wiles yaklaşımının sadeleştirilmiş bir sürümünü izlediğini söylüyor. Depo ayrıca mevcut çalışmalara atıf yapıyor: ATTRIBUTION.md dosyasında, Mathlib’in yanı sıra Imperial College London FLT projesinden veya flt-regular projesinden malzeme içeren 106 dosya listeleniyor. Yayımlanan çıktının ne üzerine kurulduğunu doğru anlatmak için bu kaynak geçmişi önem taşıyor.

Proje, çalışma sırasında 30.300 teorem önermesinin kanıtlandığını ve yaklaşık 29.500’ünün nihai ispatta kullanıldığını bildiriyor; depo ise 29.511 teorem sayfasından söz ediyor. Bunlar yeni keşfedilmiş 29.511 matematiksel sonuç değil, biçimsel bildirimler ve bağımlılıklar. Biçimsel ispat; insan ispatının uzmanların anlayışına bırakabildiği örtük adımları, türleri, tür dönüşümlerini, tanımları ve kütüphane bağımlılıklarını açıkça ortaya çıkarıyor.

Depo, kaynakların okunmaktan çok denetlenmek üzere yazıldığını belirtiyor: adlar makine tarafından oluşturulmuş, P2M gibi etiketler işlem hattına ait ve asıl belirleyici olan isim değil, önerme. Bu nedenle ispat yolu ve karşılaştırıcı, manşetteki teorem kadar önemli.

Daha önceki Lean çalışmalarını 2026 iddiasıyla bir tutmamak gerekiyor. Fermat’nın Son Teoremi’nin düzenli asallar için ele alındığı 2023 tarihli bir makale, Kummer teoreminin düzenli asallar için I. Durumu’nun eksiksiz ve sorry içermeyen biçimselleştirmesini raporlamış; II. Durum ile Kummer lemmasının ise hâlâ önemli miktarda çalışma gerektirdiğini belirtmişti. 2025 tarihli revizyon ise düzenli-asal biçimselleştirmesini bu daha dar durumun eksiksiz ispatı olarak tanımladı.

Imperial/Lean FLT projesi, modern sayı teorisini biçimselleştirmeyi yalnızca tek bir teoremi çevirmekten ibaret olmayan, daha geniş bir altyapı çalışması olarak anlatıyor. Anthropic’in yayımladığı çalışma, önceki projenin hedeflerinin artık önem taşımadığının kanıtı değil; koordineli yapay zekâ ajanlarının mevcut bir biçimsel ekosistem içinde neler yapabildiğine dair tamamlayıcı bir veri noktası olarak görülmeli.

Hangi sonuca ne ölçüde güvenilmeli?

Yalnızca haberi öğrenmek istiyorsanız, resmî duyuru ve depo projenin gerçekten var olduğunu ortaya koyuyor. Denetim yapmak istiyorsanız, sabitlenmiş derlemeyi yeniden üretin ve teorem bildirimini inceleyin. Yapay zekâ araştırmasını değerlendiriyorsanız orkestrasyonu, mevcut kütüphaneleri, önceki biçimselleştirmeleri ve hesaplama kaynaklarını sistemin parçası olarak hesaba katın.

Sıkça sorulan sorular

Claude, Fermat’nın Son Teoremi için yeni bir ispat mı keşfetti?

Hayır. Anthropic’in çıktısı, Frey, Serre, Ribet, Wiles ve Taylor-Wiles’la ilişkilendirilen yerleşik bir ispat yolunu biçimselleştiriyor. Başarı, yeni bir matematiksel çözüm bulmakta değil; makine tarafından denetlenebilir bir Lean çıktısını bu ölçekte ve hızda üretmekte.

Lean derlemesinin başarılı olması gayriresmî teoremi kanıtlar mı?

Bu, kodlanan önermenin söz konusu Lean ortamında denetlenmiş bağımlılıklardan türetilebildiğini gösterir. Ancak önermenin ve tanımlarının, iddia etmek istediğiniz gayriresmî teoremle gerçekten örtüştüğünü ayrıca doğrulamanız gerekir.

Depoda sorry veya ek aksiyomlar kullanılıyor mu?

Depo, son kontrolün sorry, ek aksiyomlar, native_decide, unsafe ve benzer kestirmeleri reddettiğini söylüyor. Beklenen aksiyom listesinde Lean’in üç standart aksiyomu bulunuyor: propext, Classical.choice ve Quot.sound. Yine de yalnızca duyuruya güvenmek yerine kontrolü kendiniz çalıştırın.

Sonucu sıradan bir dizüstü bilgisayarda yeniden üretebilir miyim?

Depoyu inceleyebilir ve kısmen derleyebilirsiniz; ancak tam doğrulama sıradan ve hafif bir iş yükü değil. Depo, derleme için 153 GB, karşılaştırıcı için 230 GB en yüksek bellek kullanımı ve yüksek disk kapasitesi gereksinimleri bildiriyor. Bu nedenle donanım, sürecin temel kısıtlarından biri.

İddiayı doğru biçimde kontrol etmek için sabitlenmiş GitHub çıktısıyla başlayın, manşetten önce teorem bildirimini okuyun ve sonucu bilinen matematiğin yapay zekâ destekli, büyük ölçekli bir biçimselleştirmesi olarak aktarın.