YZ şirketi Anthropic, Fermat’nın son teoreminin biçimselleştirilmiş bir ispatını oluşturdu. Bir grup YZ ajanının bu görevi tamamlaması sadece 11 gün sürdü ve böylece 1990’larda insanlar tarafından ortaya konulan ispatın doğruluğunu kanıtladılar.
Fermat’nın son teoremi, 1995 yılında Andrew Wiles onu ispatlayana dek yüzyıllar boyunca matematikçilerin kafasını karıştırdı. Teorem, n’nin 2’den büyük bir tam sayı olduğu durumlarda aⁿ + bⁿ = cⁿ denklemini sağlayan a, b ve c tam sayılarının var olmadığını söylüyor.
İfade etmesi kolay olsa da teoremi ispatlamak son derece zordu. Matematikçi Pierre de Fermat, bu bulmacayı 17. yüzyılda ortaya attı. Hatta bulduğunu iddia ettiği bir ispata ünlü bir atıf yaparak, bu ispatın elindeki kitabın kenar boşluklarına sığmayacak kadar büyük olduğunu söyledi.
Birçok matematikçi ispatı bulmayı denedi ancak başarısız oldu. Wiles, 1993’teki büyük buluşunu duyurmadan önce problem üzerinde yedi yıl boyunca gizlice çalıştı. İspatlar genellikle birbirinin üzerine inşa edilen uzun mantıksal argümanlar içeriyor. Tek bir adımda bile hata olursa bütün yapı çökebiliyor. İspatında bir hata bulunduğunda Wiles’ın başına gelen de tam olarak buydu; çalışma arkadaşı Richard Taylor ile birlikte bu hatayı düzeltmeleri yaklaşık bir yıllarını aldı.
Matematiksel teoremleri formelleştirmek bu soruna bir çözüm sunuyor. Teoremleri kalem kağıt dünyasından çıkarıp makinaların anlayabileceği bir yapıya (bilgisayar koduna) dönüştürüyor. Böylece makinalar mantık adımlarını sistemli bir şekilde işliyor ve tüm kusurları açığa çıkarıyor. Halihazırda Mathlib adlı merkezi bir havuzda saklanan 2 milyon satırlık biçimselleştirilmiş matematik verisi bulunuyor.
Bu yılın başlarında Londra’da YZ uzmanlarını, bilgisayar bilimcilerini ve matematikçileri bir araya getiren bir konferans, Imperial College London‘dan Kevin Buzzard tarafından düzenlendi. Buzzard, Anthropic‘in duyurusuna kadar Wiles ve Taylor’ın 100 sayfalık ispatını Lean adlı programlama dilinde biçimselleştirmeyi hedefleyen beş yıllık bir proje yürütüyordu. Buradaki amaç, ispatın doğruluğunun biçimsel olarak doğrulanabilmesi ve gelecekteki araştırmalara temel oluşturmasıydı.
Buzzard o dönemde projeye başlarken başarıdan emin olduğunu ama YZ alanındaki son gelişmelerin projenin daha önce mümkün olduğunu düşündüğünden çok daha hızlı biteceğine onu ikna ettiğini söyledi. Anthropic’in duyurusu ise bu çabayı geride bıraktı ve problemi çözüme kavuşturdu.
Buzzard, Anthropic tarafından yayımlanan açıklamasında, şirketin ortaya koyduğu ispatın “matematiğin aksiyomları dışında hiçbir varsayıma yer bırakmadığını” belirtti. Kısacası problem çözüldü.
Buzzard, “Süreç boyunca cebir, harmonik analiz, geometri ve sayılar teorisinin otomatik biçimselleştirildiğini görüyoruz ve YZ otomatik biçimselleştirme yapılarının artık üzerine yeni şeyler inşa edilebilecek kadar sağlam olduğunu anlıyoruz; ispat çok katmanlı. Eğer FLT’nin otomatik biçimselleştirilmesi şu an mümkünse, modern matematik literatürünün otomatik biçimselleştirilmesine doğru büyük bir adım atmışız demektir.” ifadelerini kullandı.
Anthropic, sonucu duyurduğu blog yazısında Claude modelinin ispatı yazmak için 11 gün boyunca kesintisiz ve otonom şekilde çalıştığını belirtti. Sürece, her birine teoremin daha küçük parçalarını ele almak gibi farklı görevler atanan çok sayıda ayrı YZ ajanı dahil oldu.
Şirket, insan uzmanların çalışmayı rayında tutmak için zaman zaman “üst düzey talimatlar” verdiğini söylüyor. Ajanlar birkaç kez “projenin durumunu gözden kaçırdı ve etkili iş birliği yapmayı bıraktı”. İlginç bir şekilde şirket; başarının, insanların matematiksel iş birlikleri için tasarlanan Prove2Me adlı aracı kullanmaya başladıktan sonra geldiğini söyledi. Bu araç, farklı ajanların kendi işlerini takip etmelerine ve bir sonraki adıma karar vermelerine yardımcı oldu.
Anthropic’in biçimselleştirmesi toplam 13 milyon satır Lean kodundan oluşuyor ve genel çalışmayı tamamlamak için gerekli adımlar olan yaklaşık 29.500 ara teoremi kapsıyor. Bu durum, ispatı Mathlib üzerinde daha önce yapılan tüm çalışmaların toplamından beş kat daha büyük yapıyor. Aynı zamanda onu şimdiye dek yazılmış en büyük Lean ispatı haline getiriyor.
Kaynak: https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/
