350 Yıllık Matematik Hikâyesi Bir Kez Daha Değişti: Yapay Zekâ Fermat’nın Son Teoremini 11 Günde Bilgisayara Doğrulattı

Bir matematik probleminin çözülmesi 350 yıldan uzun sürdü.

Çözümün bilgisayarın anlayabileceği şekilde yeniden yazılması içinse yıllar sürecek bir çalışma bekleniyordu.

Son aşama 11 gün sürdü.

Matematik tarihinin en ünlü problemlerinden Fermat’nın Son Teoremi, 1990’larda Andrew Wiles ve Richard Taylor’ın çalışmalarıyla kanıtlanmıştı. Fakat insan matematikçiler için ikna edici olan devasa matematiksel yapı, bilgisayarın en küçük mantıksal adımına kadar denetleyebileceği biçimde hiçbir zaman tamamen yazılmamıştı.

Eylül 2026’da bu da değişti.

Anthropic araştırmacıları, Claude tabanlı yapay zekâ ajanlarının büyük ölçüde otonom çalışarak Fermat’nın Son Teoremi’nin ilk eksiksiz bilgisayar denetimli formel ispatını oluşturduğunu açıkladı. Sistem bunu yapmak için yaklaşık 13 milyon satır Lean kodu üretti ve on binlerce ara teoremi ispatladı.

Fakat hikâyenin en önemli noktası “yapay zekâ Fermat’yı çözdü” değil.

Çünkü problem zaten çözülmüştü.

Asıl gelişme, matematikte “doğru olduğuna inanıyoruz” ile “bir bilgisayar bütün mantıksal zinciri baştan sona kontrol etti” arasındaki mesafenin yapay zekâ sayesinde dramatik biçimde kısalmaya başlaması.

Her şey bir kitabın kenarındaki notla başladı

Hikâye yaklaşık 1637’de Fransız matematikçi Pierre de Fermat’nın Arithmetica adlı kitabın kenarına yazdığı birkaç satırla başladı.

Pisagor teoreminden bildiğimiz denklem oldukça basittir:

a² + b² = c²

Bu denklemin pozitif tam sayılarda birçok çözümü vardır. Örneğin 3² + 4² = 5².

Fermat ise üs 2’den büyük olduğunda durumun tamamen değiştiğini ileri sürdü. Başka bir ifadeyle n, 2’den büyük bir tam sayı olduğunda aⁿ + bⁿ = cⁿ denkleminin pozitif tam sayılarda çözümü olmadığını söyledi.

Ardından matematik tarihinin en ünlü notlarından birini bıraktı: Bunun gerçekten harika bir kanıtını bulduğunu, fakat kitabın kenarındaki boşluğun kanıtı yazmak için çok dar olduğunu belirtti.

O kanıt hiçbir zaman bulunamadı.

Sonraki üç buçuk yüzyıl boyunca dünyanın en iyi matematikçileri problemi çözmeye çalıştı. Bazı özel durumlar kanıtlandı, yeni matematik alanları geliştirildi, fakat genel teorem direnmeye devam etti.

Ta ki Andrew Wiles’a kadar.

Wiles’ın yedi yıllık gizli çalışması

Andrew Wiles çocukluğundan beri Fermat’nın problemine ilgi duyuyordu. Yetişkinliğinde profesyonel bir matematikçi olduğunda ise problemi çözmek için doğrudan Fermat’nın denklemine saldırmak yerine çok daha derin bir matematiksel bağlantıyı kullandı.

1986’dan itibaren yaklaşık yedi yıl boyunca büyük ölçüde gizlice çalıştı.

1993’te Cambridge’de verdiği derslerin sonunda Fermat’nın Son Teoremi’nin kanıtını açıkladığında matematik dünyasında büyük heyecan yaşandı. Fakat kısa süre sonra kanıtta ciddi bir boşluk bulundu.

Wiles ve Richard Taylor bu problemi yaklaşık bir yıl daha çalışarak giderdi. Düzeltilmiş ispat 1995’te yayımlandı ve Fermat’nın yaklaşık 350 yıllık problemi sonunda çözüldü.

Matematik açısından hikâye burada bitebilirdi.

Bilgisayar açısından ise bitmemişti.

Çünkü matematikçinin “kanıt” dediği şey ile bilgisayarın “kanıt” olarak kabul ettiği şey aynı değil.

Bir matematikçinin atladığı tek satır, bilgisayar için yüzlerce adım olabilir

Matematik makaleleri bilgisayar programları gibi yazılmaz. Uzman okuyucunun bildiği sonuçlar tekrar tekrar açıklanmaz. Bazı çıkarımlar “açıktır”, “buradan kolayca görülür” veya “standart argüman uygulanır” gibi ifadelerle geçilebilir.

Bunun nedeni matematikçilerin dikkatsiz olması değil; matematiksel iletişimin böyle çalışmasıdır. Bir uzman diğer uzmanın hangi adımları tamamlayabileceğini bilir.

Bilgisayar ise bunu yapmaz.

Bir teoremi Lean gibi bir ispat asistanına verdiğinizde sistem her mantıksal bağlantının açık biçimde kurulmasını ister. Tanımlar kesin olmalıdır. Kullanılan önceki teoremler belirtilmelidir. Tipler uyuşmalıdır. Bir adım öncekinin gerçekten sonucu değilse sistem ilerlemenize izin vermez.

Bu işleme formelleştirme deniyor.

Fermat’nın Son Teoremi gibi modern matematiğin çok sayıda derin alanına dayanan bir ispatı formelleştirmek bu nedenle devasa bir görev.

Mesele yalnızca Wiles’ın makalesindeki cümleleri bilgisayar koduna çevirmek değil. Wiles’ın kullandığı matematiksel dünyanın önemli bölümünü de bilgisayarın anlayacağı biçimde kurmanız gerekiyor.

İnsanlar zaten bu işe başlamıştı

Bu noktada 11 günlük başarıyı doğru değerlendirmek önemli.

Yapay zekâ boş bir bilgisayarın karşısına oturup 350 yıllık matematik tarihini sıfırdan üretmedi.

Lean ekosisteminde yıllardır binlerce matematiksel tanım ve teorem biriktiriliyor. Bunların önemli bölümü açık kaynaklı Mathlib kütüphanesinde bulunuyor. Fermat’nın Son Teoremi için de Imperial College London’dan matematikçi Kevin Buzzard’ın liderliğinde 2024’te büyük bir formelleştirme projesi başlatılmıştı.

İnsan matematikçiler gerekli altyapının önemli parçalarını zaten oluşturuyordu. Ayrıca teoremin bazı özel durumlarının bilgisayar tarafından doğrulanmış formel kanıtları daha önce tamamlanmıştı.

Anthropic’in sistemi bütün bu insan emeğinin üzerine kuruldu.

Fakat geriye kalan mesafe hâlâ olağanüstü büyüktü.

Claude tabanlı çoklu ajan sistemi bu noktada devreye girdi.

11 günde 13 milyon satır

Anthropic araştırmacısı Tianyi Peng ve ekibi, Claude’un Fermat’nın Son Teoremi’nin formelleştirilmesinde ne kadar ilerleyebileceğini görmek istedi.

Sonuç beklediklerinden çok daha ileri gitti.

Çok sayıda Claude ajanı farklı matematiksel görevler üzerinde paralel biçimde çalıştı. Bazıları tanımları oluşturdu, bazıları ara teoremleri ispatladı, diğerleri bu sonuçları kullanarak daha karmaşık adımlara ilerledi.

Toplam çalışma süresi yalnızca 11 gün oldu.

Ortaya yaklaşık 13 milyon satırlık Lean kodu çıktı.

Sistem çalışma sırasında yaklaşık 30.300 teorem ispatladı ve bunların yaklaşık 29.500’ü nihai Fermat ispatında kullanıldı.

Bu ölçeği anlamak için ilginç bir karşılaştırma var: ortaya çıkan Fermat formalizasyonu, üzerine inşa edildiği Mathlib’in kendisinden satır sayısı bakımından beş kattan fazla büyük.

Fakat milyonlarca satır kod yazmak tek başına matematiksel başarı anlamına gelmez.

Asıl önemli soru şuydu:

Doğru mu?

Bu kez cevabı başka bir yapay zekâ vermedi

Sonucun en önemli taraflarından biri burada ortaya çıkıyor.

Claude kendi ödevini kontrol edip “doğru” demedi.

Lean’in çekirdeği ispatı kontrol etti.

Formel ispat sistemlerinde çekirdek, sistemin en küçük ve güvenilmesi gereken bölümüdür. Yapay zekâ ne kadar karmaşık kod üretirse üretsin, nihai matematiksel adımlar bu küçük doğrulama mekanizmasından geçmek zorunda.

Anthropic’in yayımladığı yapıda Fermat’nın Son Teoremi’nin ispatı standart Lean aksiyomlarının dışında gizli bir varsayıma dayanmıyor. Eksik kanıtları geçici olarak kabul ettirmek için kullanılan “sorry” gibi kaçış mekanizmaları da nihai sonuçta bulunmuyor.

Daha da önemlisi çalışma ikinci, bağımsız bir kontrol mekanizmasından geçirildi. Rust ile yazılmış nanoda adlı bağımsız Lean çekirdeği, dışa aktarılan ortamda bir milyondan fazla bildirimi kontrol ederek hata bulmadı.

Yani burada “yapay zekâ doğru olduğunu düşünüyor” türünden olasılıksal bir güven söz konusu değil.

Bilgisayar, belirlenmiş mantıksal kurallar altında ispat zincirini mekanik olarak kontrol ediyor.

Bu ayrım yapay zekâ çağında matematik açısından son derece önemli olabilir.

Çünkü AI daha fazla matematik üretmeye başlarsa yeni problem doğrulamak olacak

Bugünün yapay zekâ sistemleri matematik problemleri çözebiliyor, yeni ispat yolları önerebiliyor ve giderek daha karmaşık araştırma görevlerine katılabiliyor.

Bu eğilim devam ederse bilim dünyası garip bir problemle karşılaşabilir.

Bir yapay zekâ sistemi bir günde binlerce matematiksel sonuç üretebilir.

Ama insanların bunların tamamını kontrol etmesi aylar veya yıllar sürebilir.

Bu durumda yapay zekânın matematik üretme hızı, insanların matematiği doğrulama hızını aşar.

Formel ispat sistemleri bu darboğaz için olası bir çözüm sunuyor.

Yapay zekâ yalnızca sonucu üretmek yerine sonucu Lean gibi bir sistemin denetleyebileceği biçimde sunarsa, güvenin kaynağı AI’ın kendisi olmaktan çıkar.

Yapay zekâ önerir.

Formel sistem kontrol eder.

İnsan ise hangi problemin önemli olduğuna, kullanılan matematiğin ne ifade ettiğine ve sonucun daha büyük bilimsel resimde nereye oturduğuna karar verir.

Bu üçlü yapı geleceğin matematik araştırmasının önemli modellerinden biri olabilir.

Peki Claude yeni matematik mi yaptı?

Fermat örneğinde cevap büyük ölçüde hayır.

Claude’un görevi yeni bir Fermat kanıtı keşfetmek değildi. Sistem Frey, Serre, Ribet, Wiles ve Taylor-Wiles tarafından oluşturulan bilinen matematiksel yolu bilgisayarın kontrol edebileceği biçimde yeniden kurdu.

Bu ayrım önemli, çünkü “AI 350 yıllık problemi 11 günde çözdü” demek yanlış olur.

Problem yaklaşık otuz yıl önce çözülmüştü.

Fakat bu, 11 günlük sonucu önemsiz hale getirmiyor.

Tam tersine matematikte uzun süredir insan emeğinin en yoğun olduğu alanlardan birinin otomasyona açılabileceğini gösteriyor.

Bir matematikçinin yazdığı ispatı formel dile çevirmek yaratıcı matematiğin gölgesinde kalan teknik bir iş gibi görünebilir. Oysa modern bir teorem söz konusu olduğunda yüzlerce tanımı, binlerce ara sonucu ve farklı matematik alanlarını kusursuz biçimde birbirine bağlamak gerekir.

Fermat’nın Son Teoremi bunun uç örneklerinden biri.

Ve artık ilk kez bütün zincir bir bilgisayar tarafından baştan sona kontrol edilebiliyor.

Fermat’nın hikâyesi belki de üçüncü kez değişiyor

Fermat’nın Son Teoremi’nin tarihinde üç farklı dönem görmek mümkün.

İlki 1637 civarında başladı: Fermat bir iddia ortaya attı ve insanlık bunun doğru olup olmadığını bilmiyordu.

İkinci dönem 1990’larda Wiles ve Taylor ile başladı: İnsan matematikçiler teoremin doğru olduğunu kanıtladı.

Şimdi üçüncü dönem başlıyor olabilir.

2026’da teorem yalnızca insanların okuyup değerlendirdiği bir matematik makalesi olmaktan çıktı. Bütün mantıksal yapısı bilgisayarın denetleyebileceği formel bir nesneye dönüştürüldü.

Bu, Fermat’nın Son Teoremi’nin daha doğru hale geldiği anlamına gelmiyor. Matematikçiler Wiles’ın kanıtından zaten emindi.

Değişen şey kanıt ile makine arasındaki ilişki.

Ve bu dönüşüm yalnızca Fermat’yla sınırlı kalmayabilir.

Bugün milyonlarca satırlık bir formalizasyon için onlarca yapay zekâ ajanı çalışıyor. Yarın bilimsel makalelerin yanında bilgisayar tarafından doğrulanabilir ispat dosyalarının yayımlanması sıradan hale gelebilir.

Bir matematikçi yeni bir teorem ortaya koyduğunda “İspat burada” demek yeterli olmayabilir.

Yanında başka bir şey daha bulunabilir:

“Bilgisayar da bütün adımları kontrol etti.”

Fermat’nın yaklaşık 350 yıl önce bir kitabın kenarına sığdıramadığını söylediği kanıt, sonunda 13 milyon satırlık bilgisayar koduna dönüştü.

Belki de hikâyenin en güzel ironisi bu.

Bir zamanlar bir kitabın kenarı kanıt için fazla küçüktü.

Şimdi kanıt, bir insanın baştan sona okumak istemeyeceği kadar büyük.

Ama bilgisayarın kontrol edebileceği kadar kesin.