Fermat’ın meşhur son teoremi bu kez yapay zeka tarafından da kanıtlandı

İngiliz matematikçi Andrew Wiles aslında Fermat'ın son teoremini 1994 yılında kanıtlamıştı ama bu kez Anthropic devreye girdi ve Wiles'ın kanıtını 13 bin satırlık bir bilgisayar koduyla "formelize" etti. Matematikçiler şaşkın.

Son yarım yüzyılın en ünlü matematiksel başarılarından biri olan Fermat’nın Son Teoremi, yapay zeka sohbet robotu Claude’un gelişmiş bir prototipi kullanılarak ilk kez bilgisayar tarafından doğrulanmış bir koda dönüştürüldü.

Okulda gördüğümüz Pisagor teoreminde a kare + b kare = c kare eşitliğini sağlayan tam sayılar bulmak son derece kolaydır. Ancak Fransız matematikçi Pierre de Fermat 1637’de şu iddiada bulundu: Üs sayısı 2’den büyük olduğunda (n > 2), yani x n + y n = z n denkleminde, bu eşitliği sağlayan hiçbir pozitif x, y, z tam sayısı bulunamaz.

Fermat’ın teoremi işte buydu. Anlaması bu kadar basit olan bir iddianın eksiksiz biçimde kanıtlanması insanlığın 350 yıldan uzun süresini aldı ve nihayet 1994’te başarıldı.

Şimdi, kanıtlamadan 32 yıl sonra bu kez aynı Fermat’ın Son Teoremi bir başka büyük başarının daha konusu oldu.

New Jersey, Piscataway’deki Rutgers Üniversitesi’nde sayılar teorisyeni olan Alex Kontorovich, bir makinenin insan matematikçilerin çalışmasını 13 milyon satırlık sarsılmaz bir ispata dönüştürmesinin “aklını başından aldığını” söylüyor. San Francisco merkezli Anthropic AI firması bu tarihi gelişmeyi 4 Eylül’de duyurdu. Model, insanların 10 yılını alması beklenen bir projeyi sadece 11 günde tamamladı.

Bu sonuç, yapay zekanın matematikçilerin çalışmalarını denetlemede ve yeni matematiksel akıl yürütmeler üretmede giderek daha önemli bir rol oynayacağını gösteriyor. Mevcut ilerleme hızı göz önüne alındığında, yapay zekanın yakında tüm matematik külliyatını inceleyerek iyi bilinen bazı sonuçların hatalı olduğunu ortaya çıkarması işten bile değil. Imperial College London’dan matematikçi Kevin Buzzard, “İki yıl önce bu sadece bir hayaldi,” diyor.

Matematikçiler, yapay zekanın matematiksel becerilerinin artma hızından giderek daha fazla büyüleniyor. Buna, teknolojinin ispatları “formalize etme” —yani matematiksel argümanları doğal dilden Lean gibi programlama dillerine, bilgisayarca doğrulanabilir formal koda çevirme— yeteneği de dahil.

Şubat ayında yapay zeka, Maryna Viazovska’nın 8 ve 24 boyutlu uzaylarda kürelerin en verimli paketlenme yollarına dair Fields Madalyalı çalışmasını onaylayarak formalizasyon alanında başka bir dönüm noktasına ulaşmıştı. Ancak Buzzard, Fermat’nın Son Teoremi üzerindeki çalışmanın çok daha üst seviyede bir karmaşıklığa sahip olduğunu belirtiyor: “Bu çalışma belki de bir kat daha zordu.”

Kanada Toronto Üniversitesi’nden sayılar teorisyeni Daniel Litt de bu görüşe katılıyor: “Fermat’nın Son Teoremi’ni formalize edebiliyorlarsa, muhtemelen her şeyi formalize edebilirler.”

Fermat’nın Son Teoremi’nin 1994 yılında Andrew Wiles ve Richard Taylor tarafından tamamlanan orijinal ispatı, 20. yüzyıl matematiğinin nirengi noktalarından biriydi.

Bu denklemi tek başına çözmek —veya hiçbir çözümü olmadığını bilmek— pratik bir kullanım sunmasa da, Wiles’ın problemi çözmek için geliştirdiği teknikler matematiğin birbirinden uzak alanlarını bir araya getirmeye yardımcı oldu. Bu ispat, Wiles’a 2016 yılında matematiğin en prestijli ödüllerinden biri olan Abel Ödülü’nü kazandırdı.

Matematikçiler ispat yaparken Türkçe veya İngilizce gibi günlük dilleri ve zihinlerindeki mantıksal kısaltmaları kullanırlar. Ancak insan zihni gözden detay kaçırmaya müsaittir. Formalizasyon, insan dilindeki bu karmaşık matematiksel mantığı, bilgisayarların (Lean gibi mantık dillerinin) anlayabileceği aşırı detaylı bir kod yapısına dönüştürmektir. Bilgisayar yazılımı bu kodu satır satır tarayarak tek bir mantık hatası bile olmadığını%100 kesinlikle onaylar.

Deneyiminizi iyileştirmek, tanımlama bilgilerini, sitemizin doğru şekilde çalışmasını sağlamak, içerikleri ve reklamları kişiselleştirmek, sosyal medya özellikleri sunmak ve site trafiğimizi analiz etmek için yasal düzenlemelere uygun çerezler (cookies) kullanıyoruz.