Claude, Fermat teoremini Lean’de doğruladı: yeni bir ispat değil
Anthropic, 4 Eylül 2026’da Claude’un Fermat’ın Son Teoremi için hazırladığı uçtan uca Lean formalleştirmesini yayımladı. Anthropic’in araştırma duyurusuna göre Claude ajanları 11 gün boyunca büyük ölçüde özerk çalıştı; yaklaşık 13 milyon satır Lean kodu yazdı, 30.300 ara teoremi kanıtladı ve bunların yaklaşık 29.500’ünü nihai yapıda kullandı. Çalışma yaklaşık altı milyar model çıktı tokenı tüketti.
4 Eylül’de yayımlanan sonuç, Claude’un Fermat’ın Son Teoremi için bağımsız ve yeni bir matematiksel ispat keşfettiği anlamına gelmiyor. Lean uzmanı ve mevcut formalleştirme projesinin lideri Kevin Buzzard, kendi teknik değerlendirmesinde kod tabanını derlediğini ve comparator denetimini çalıştırdığını belirtiyor; çalışmanın erken dönem Wiles–Taylor–Wiles literatürünü sadakatle izlediğini ve matematiğe yeni bir sonuç eklemediğini söylüyor.
Yeni ispat ile formalleştirme arasındaki fark
Matematiksel ispat, bir teoremi kabul edilmiş tanım ve sonuçlara bağlayan argümandır. Fermat’ın Son Teoremi’ni sonuçlandıran matematiksel yol; Frey, Serre ve Ribet’in sonuçları ile Andrew Wiles ve Richard Taylor’ın çalışmalarına dayanıyor. Claude bu yolu değiştiren yeni bir fikir, daha kısa bir argüman veya daha önce bilinmeyen bir teorem ortaya koymadı.
Claude’un yaptığı iş formalleştirme: İnsanlar için yazılmış ispat çizgisini, Lean’in her adımını denetleyebileceği kesin tanımlara ve mantıksal çıkarımlara dönüştürmek. Bir matematikçi metinde “standart sonuçtan çıkar” denilen geçişi tamamlayabilir; Lean ise kullanılan tanımı, ara önermeyi ve bütün bağımlılıkları açık biçimde görmek zorunda.
Bu nedenle milyonlarca kod satırı, tek başına matematiksel yeniliğin ölçüsü değil. Boyut, insan anlatımında örtük bırakılabilen ayrıntıların makine için görünür hâle getirilmesinden ve gereken biçimsel altyapının kurulmasından kaynaklanıyor. Haber değeri teoremin yeniden çözülmesinde değil, çok katmanlı bir ispat çizgisinin kısa sürede baştan sona makinece kontrol edilebilir duruma getirilmesinde.
Lean doğrulaması neyi garanti ediyor?
Lean’de dosyaların bulunması veya kodun çalışıyor görünmesi yeterli değil. Sistemin küçük çekirdeği, her bildirimin izin verilen mantık kuralları ve daha önce denetlenmiş bildirimlerden çıkıp çıkmadığını kontrol ediyor. Başarılı derleme, biçimsel zincirin belirtilen sistem içinde geçerli olduğunu gösteriyor; fakat metnin öğretici, kısa veya insan için kolay anlaşılır olduğunu garanti etmiyor.
Yayımlanan Lean 4 deposu, nihai teoremin yalnızca Lean’in üç standart aksiyomuna—propext, Classical.choice ve Quot.sound—dayandığını belgeliyor. Varsayılan denetim, tamamlanmamış ispat yerine kullanılan “sorry” ifadesini veya sonradan eklenmiş bir aksiyomu kabul etmiyor. Comparator, kanıtlanan ifadeyi Mathlib’deki Fermat’ın Son Teoremi ifadesiyle eşleştirdi; Rust ile yazılmış bağımsız nanoda çekirdeği de aynı ortamda 1.052.234 bildirimi hatasız kabul etti.
Bu katmanlar iki temel riski azaltıyor: mantıksal olarak geçersiz bir zincirin kabul edilmesi ve gerçek teorem yerine ona benzeyen daha zayıf bir ifadenin kanıtlanması. Yine de güven bütünüyle ortadan kalkmıyor; Lean veya nanoda çekirdeğinin ve kullanılan denetim araçlarının doğru çalıştığı varsayılıyor. Ara teoremlerin insan dilindeki adlarıyla gerçekten aynı şeyi anlattığını da çekirdek denetlemiyor; belirleyici olan ad değil, biçimsel ifade.
On bir günlük çalışma insan altyapısının üzerine kuruldu
“Büyük ölçüde özerk” ifadesi, sıfır insan katkısı demek değil. Anthropic araştırmacısı Tianyi Peng süreçte zaman zaman hangi matematiksel bileşenlerin öncelikli olduğuna dair üst düzey yönlendirmeler yaptı. Çok sayıda Claude ajanı ise tanımları oluşturmak, alt sonuçları kanıtlamak ve tamamlanan parçaları daha üst düzey teoremlerde birleştirmek için paralel çalıştı.
Bu koordinasyonu Peng ve Columbia University’deki çalışma arkadaşlarının geliştirdiği Prove2Me platformu sağladı. Platform, teoremleri ve bağımlılıklarını yönlü döngüsüz bir grafikte tutarak ajanların projenin durumunu izlemesine, uygun alt probleme yönelmesine ve daha önce tamamlanan sonuçları yeniden kullanmasına yardımcı oldu. İlk çoklu ajan denemelerinin bir bölümü, ajanlar ortak proje durumunu izlemekte zorlandığı için sonuç vermedi.
Çalışma ayrıca boş bir kütüphanede başlamadı. Lean’in topluluk tarafından geliştirilen Mathlib altyapısını, Imperial College London öncülüğündeki Fermat projesinin parçalarını ve “flt-regular” çalışmasından alınan malzemeyi kullandı. Dolayısıyla 11 gün, Fermat teoreminin matematiksel temelini sıfırdan kurma süresi değil; yıllar içinde insanlarca üretilen matematik ve açık kaynaklı Lean altyapısı üzerine eklenen yoğun formalleştirme süresi.
Açık depoyu yeniden doğrulamak neden zor?
Kodun açık olması, bütün denetimlerin sıradan bir bilgisayarda kolayca tekrarlanabileceği anlamına gelmiyor. Depoda belgelenen örnek çalıştırmada 60.475 modülün 96 paralel işle derlenmesi 5 saat 32 dakika sürdü ve bellek kullanımı 153 GB ile zirve yaptı. Comparator denetimi 14 saat 46 dakika çalıştı, 230 GB tepe belleğe ulaştı; depo bu aşama için 300 GB kullanılabilir bellek öneriyor.
Derleme ortamı yaklaşık 67 GB disk alanı istiyor; süreçte üretilip daha sonra silinebilen C dosyaları için yaklaşık 220 GB daha gerekebiliyor. Bu rakamlar proje ekibinin belirli donanım ve paralellik düzeyindeki çalıştırmasına ait. Farklı bir sistemde süre ve kaynak tüketimi değişeceği için bunlar evrensel bir performans ölçümü değil.
Ortaya çıkan paket kamuya açık, üç ayrı denetim katmanından geçirilmiş ve araştırma eseri olarak yayımlanmış durumda; depo sürdürülen bir yazılım ürünü değil ve katkı kabul etmiyor. Kanıtlanan sonuç Fermat’ın Son Teoremi, fakat kullanılan matematiksel rota mevcut literatüre dayanıyor. Bundan sonra uzman incelemesi, formalleştirmenin okunabilirliğine, kaynaklarının izlenmesine ve aynı ölçekteki çalışmaların daha az kodla ve daha erişilebilir donanımla yeniden üretilebilir olup olmadığına odaklanacak.
Ayrıca okuyun:
Bültenimize abone olun
En son Web3, yapay zekâ ve kripto haberleri doğrudan gelen kutunuza gelsin.