Yapay zeka şirketi Anthropic, Fermat’ın Son Teoremi için 11 günde formel bir kanıt geliştirdi. Bu, matematik tarihindeki önemli bir gelişme.
Yapay zeka alanında önemli bir gelişme yaşandı. Anthropic adlı şirket, Fermat’ın Son Teoremi için formel bir kanıt geliştirdi. Bu süreç, sadece 11 gün sürdü ve 1990’larda insan tarafından bulunan kanıtın doğruluğunu da onayladı.
Fermat’ın Son Teoremi, matematikçileri yüzyıllar boyunca düşündüren bir problem oldu. 1995 yılında Andrew Wiles tarafından kanıtlanan bu teorem, a, b ve c tam sayılarının aⁿ + bⁿ = cⁿ eşitliğini sağlayamayacağını ifade eder. Teorem, söylenmesi kolay olsa da, kanıtlanması son derece zordu. 17. yüzyılda Pierre de Fermat tarafından ortaya atılan bu problem, Fermat’ın bulduğunu iddia ettiği bir kanıtın, yazdığı kitabın kenarına sığmayacak kadar büyük olduğunu söylemesiyle ünlüdür.
Birçok matematikçi bu teoremi kanıtlamak için çaba sarf etti fakat başarılı olamadı. Wiles, bu problemi gizli bir şekilde yedi yıl boyunca çalışarak çözmeyi başardı ve 1993’te büyük bir ilerleme kaydetti. Kanıtlar genellikle birbiri üzerine inşa edilen uzun mantıksal argümanlar içerir; bu nedenle tek bir adımda yapılan bir hata, tüm kanıtın çökmesine neden olabilir. Wiles’ın kanıtında da bir hata bulunmuş ve bu hatayı düzeltmek bir yıl almıştır.
Matematiksel teoremleri formel hale getirmek, bu tür sorunların üstesinden gelmenin bir yolu olarak görülüyor. Bu süreç, teoremleri kağıt ve kalemden çıkararak bilgisayar kodu haline getiriyor ve makinelerin mantığı sistematik bir şekilde incelemesine olanak tanıyor. Böylece olası hatalar da ortaya çıkabiliyor. Şu anda Mathlib adlı merkezi bir depoda 2 milyon satır formel matematik bulunuyor.
Bu yılın başlarında, Londra’da AI uzmanları, bilgisayar bilimcileri ve matematikçilerin katıldığı bir konferans düzenlendi. Kevin Buzzard tarafından yapılan bu etkinlik, Wiles ve Taylor’ın 100 sayfalık kanıtını Lean adlı bir programlama dilinde formel hale getirmek için beş yıllık bir projeydi. Anthropic’ın duyurusundan önce, Buzzard projenin daha hızlı tamamlanacağına inanıyordu. Ancak Anthropic’ın başarısı, bu çabayı geride bıraktı.
Buzzard, Anthropic’ın kanıtının ‘matematiğin aksiyomları dışında hiçbir varsayım bırakmadığını’ belirtti. Yani, sorun çözülmüş durumda. Anthropic, Claude modelinin 11 gün boyunca sürekli ve otonom bir şekilde çalışarak kanıtı yazdığını açıkladı. Çeşitli AI ajanları, teoremin daha küçük parçalarıyla ilgilenerek farklı görevler üstlendi. İnsan uzmanlar, süreci yönlendirmek için zaman zaman ‘yüksek seviye talimatlar’ verdiler.
Anthropic’ın formelleştirmesi, 13 milyon satır Lean kodu içeriyor ve yaklaşık 29,500 ara teoremi kapsıyor. Bu, Mathlib’deki önceki tüm çalışmalardan beş kat daha büyük bir kanıt oluşturuyor ve Lean dilinde yazılmış en büyük kanıt olma özelliğini taşıyor.
Kaynak: New Scientist
