Claude, Fermat teoremini 11 günde resmileştirdi; yeni ispat bulmadı
Anthropic, 4 Eylül 2026’da Claude tabanlı çok ajanlı bir sistemin Fermat’ın Son Teoremi için uçtan uca, bilgisayar tarafından denetlenebilen bir Lean formalizasyonu ürettiğini duyurdu. Şirkete göre çalışma 11 gün sürdü ve ortaya yaklaşık 13 milyon satırlık bir yapı çıktı.
4 Eylül’de duyurulan sonuç, Claude’un Fermat’ın Son Teoremi için yeni bir matematiksel ispat bulduğu anlamına gelmiyor. Claude, daha önce insanlar tarafından kurulmuş ispat yolunu Lean’in adım adım denetleyebileceği biçime aktardı; yenilik teoremin çözümünde değil, formalizasyonun ölçeği ve hızında.
Claude 11 günde neyi tamamladı?
Claude’un görevi, insanlar için yazılmış bir ispatı özetlemek veya doğru ilan etmek değildi. Sistem; tanımları, ara sonuçları ve bunların bağımlılıklarını Lean çekirdeğinin kontrol edebileceği kadar açık biçimde kurmak zorundaydı. İnsanların ortak bilgiye dayanarak atladığı adımlar, biçimsel bir ispatta açık mantıksal gerekçelere bağlanır.
Anthropic’in araştırma açıklamasına göre onlarca Claude ajanı Prove2Me adlı ortak çalışma ortamında 11 gün boyunca çalıştı; sistem 30.300 ara teorem için bilgisayarca denetlenebilir ispat üretti, bunların yaklaşık 29.500’ü nihai yapıda kullanıldı ve Lean kodunun toplamı yaklaşık 13 milyon satıra ulaştı. Şirket ayrıca bunun Mathlib’den beş kattan büyük olduğunu, ancak Mathlib’in daha özlü ve insan denetiminden geçmiş yapısıyla doğrudan verimlilik karşılaştırması sayılamayacağını belirtiyor.
Prove2Me, teorem ifadelerini yönlendirilmiş çevrimsiz bir bağımlılık grafiğinde düzenledi. Ajanlar böylece hangi alt problemlerin tamamlandığını, hangi sonuçların başka teoremlere bağlı olduğunu ve sırada hangi işlerin bulunduğunu izleyebildi. Anthropic’in anlatımına göre önceki girişimler, ajanların proje durumunu kaybetmesi ve etkili biçimde eşgüdüm kuramaması nedeniyle hedefe ulaşamamıştı.
Neden yeni bir matematiksel ispat değil?
Yeni bir ispat, bilinen bir sonuca farklı bir matematiksel argüman, yöntem veya kavramsal güzergâh sunar. Claude’un çalışması ise Frey, Serre, Ribet, Wiles ve Taylor-Wiles çizgisindeki bilinen matematiği izliyor; kullanılan ana anlatım Henri Darmon, Fred Diamond ve Richard Taylor’ın Wiles yaklaşımını sadeleştiren açıklamasına dayanıyor.
AI Stack Current’ın teknik incelemesi de yayımlanan nesneyi yeni bir çözüm değil, mevcut ispat güzergâhının makinece denetlenebilir formalizasyonu olarak tanımlıyor. Başka bir deyişle Claude, Lean içinde geçerli bir ispat nesnesi oluşturdu; daha önce çözülmemiş bir problemi çözmedi ve Wiles’ın çalışmasından bağımsız yeni bir yol keşfetmedi.
Fermat’ın Son Teoremi, n değeri 2’den büyük olduğunda pozitif tam sayılar için a üzeri n artı b üzeri n eşittir c üzeri n denkleminin çözümü bulunmadığını söyler. Andrew Wiles’ın Richard Taylor ile tamamladığı çalışma teoremi 1990’larda zaten kanıtlamıştı. Yeni gelişme, bu sonucun ve ona giden geniş matematiksel altyapının bilgisayarın denetleyebileceği biçimde bir araya getirilmesidir.
13 milyon satırın arkasındaki insan emeği
Toplam satır sayısı, Claude’un 13 milyon satırlık yapıyı mevcut formal matematikten bağımsız olarak ürettiğini göstermiyor. Proje Mathlib üzerine kuruldu; ayrıca Imperial College London’daki Fermat formalizasyonu ile flt-regular projesinden alınan veya uyarlanan bölümler içeriyor. Formal matematikte doğrulanmış kütüphaneleri ve önceki teoremleri yeniden kullanmak olağan bir yöntem olsa da bu bağımlılık, başarının kapsamını doğru anlatmak için önemli.
Yayımlanan deponun teknik belgeleri, Imperial College London FLT projesi veya flt-regular kaynaklı malzeme içeren 106 dosya ile Mathlib metnini yeniden üreten 23 dosya bulunduğunu kaydediyor. Bunlar dosya sayılarıdır; yeniden kullanılan satırların 13 milyon satır içindeki kesin oranını vermiyor. Bu nedenle mevcut bilgilerden Claude’a ya da önceki insan çalışmalarına ait kesin bir yüzde çıkarmak mümkün değil.
Aynı depo, yapının yalnızca bir dil modelinin ürettiği ikna edici metinden ibaret olmadığını da gösteriyor. Açıklanan denetim zincirinde 60.475 modül Lean çekirdeğinden geçirildi; Comparator, sonuç ifadesini Mathlib’deki standart Fermat ifadesiyle karşılaştırdı ve Rust ile yazılmış bağımsız nanoda çekirdeği 1.052.234 bildirimi hata vermeden kabul etti. Buradaki “bağımsız” ifadesi ikinci çekirdeğin ayrı bir yazılım uygulaması olduğunu anlatıyor; bütün üretim sürecinin dış bir ekip tarafından yeniden gerçekleştirildiği anlamına gelmiyor.
Lean’in kabulü neyi garanti ediyor, neyi etmiyor?
Lean çekirdeğinin kabulü, sunulan ispat terimlerinin belirtilen tanımlar, önceki sonuçlar ve izin verilen aksiyomlardan mantıksal olarak çıktığını gösterir. Bu, Claude’un kendi cevabına güven bildirmesinden farklıdır: Model ikna edici bir açıklama yazsa bile biçimsel kuralları karşılamayan bir yapı çekirdek tarafından kabul edilmez.
Ancak makine denetimi sınırsız bir kesinlik vaadi değildir. Güvence, biçimsel teorem ifadesinin insanların kanıtlamak istediği matematiksel iddiayı doğru temsil etmesine, çekirdeğin ve kullanılan doğrulama araçlarının sağlamlığına bağlıdır. Lean ayrıca ispatın insanlar için anlaşılır, zarif, kısa veya matematiksel bakımdan özgün olduğuna karar vermez; yalnızca tanımlanmış mantıksal çerçevede geçerli olup olmadığını denetler.
Dolayısıyla yayımlanan çalışmanın doğrulanmış sınırı nettir: Claude, bilinen Fermat ispat güzergâhını büyük ölçekli bir Lean yapısına dönüştürdü ve bu yapı açıklanan çekirdek kontrollerinden geçti. Sonuç, otomatik formalizasyon kapasitesi açısından önemli bir mühendislik başarısıdır; fakat Claude’un yeni bir Fermat ispatı bulduğunu veya aynı hızla açık matematik problemlerini çözebileceğini göstermiyor. Bundan sonraki değerlendirme, deponun başka ekiplerce yeniden derlenmesi, formal ifade ile matematiksel anlatım arasındaki bağın incelenmesi ve benzer yöntemin mevcut ispat yolu bulunmayan problemlerde nasıl sonuç vereceğinin görülmesiyle derinleşecek.
Ayrıca okuyun:
Bültenimize abone olun
En son Web3, yapay zekâ ve kripto haberleri doğrudan gelen kutunuza gelsin.