Claude'nin Fermat formalizasyonu ve yapay zekâ destekli bir kanıt, matematiğin geleceğine dair tartışma başlattı

Anthropic'in Claude'sunun Lean proof assistant'ta Fermat'ın Son Teoremi'nin formalizasyonunu tamamladığı hafta, ayrı bir preprint yaklaşık yarım yüzyıldır açık kalan bir geometri kestirimini, bir yapay zekâ sisteminden açıkça destek alarak kanıtlayan bir çalışmayı yayımladı. Her iki gelişme, eğitim almış bir matematikçi tarafından kaleme alınan, Hacker News'in ana sayfasına çıkan ve araştırma matematiğinin sessizce bir eşiği aştığını savunan mbmccoy.dev'deki bir blog yazısında bir araya getiriliyor.

Fermat'ın Son Teoremi, makine doğrulamalı

Fermat'ın Son Teoremi — iki den büyük herhangi bir üs için a üzeri n artı b üzeri n'in c üzeri n'e eşit olmasını sağlayan üç pozitif tam sayı olmadığı iddiası — insanlığın çözmesine üç yüzyıldan fazla sürdü ve Andrew Wiles'ın 1990'lardaki kanıtı dosyayı kapattı. Blog yazısına göre Claude, bu kanıtı artık Lean'de formalize etmeyi bitirdi; yani argüman, her mantıksal adımın insan hakemlere değil yazılıma doğrulatılacak şekilde yeniden yazıldı.

Bir kanıtı formalize etmek, onu keşfetmekle aynı şey değil ve teorem zaten kanıtlanmıştı. Ama Wiles'ın argümanı modern sayılar teorisinin derin bir yığınına dayanıyor ve onu tamamen makine doğrulamalı bir forma dönüştürmek büyük çaplı bir formal matematik projesi. Bir yapay zekâ sisteminin bunu tamamlaması, yalnızca taktik öneren modellerden, büyük doğrulama çabalarını büyük ölçüde kendi başına yürütebilen sistemlere geçişe işaret ediyor.

1974 kestirimi, Codex ile kanıtlandı

İkinci sonuç, yazarın kendi kariyerine daha yakın düşüyor. Hunan Üniversitesi'nden Wang ve Wu imzalı bir preprint, yazarın yaklaşık 1974'ten beri açık kalan, integral geometrisinin özelleşmiş ama önemli bir parçası olarak tanımladığı Küresel Hadwiger Kestirimi'ni kanıtlıyor. Yazar, bu kestirimi yüksek lisans döneminde denemiş ve bu yılın başlarında yapay zekâ desteğiyle tekrar denemiş, ancak başarılı olamamıştı.

Makalenin teşekkür bölümünde, OpenAI'nin Codex'inin kanıt detaylarını geliştirme, boşlukları ve açıklama gerektiren noktaları belirleme, metni organize etme ve dizme ile İngilizce düzenlemesinde yardımcı olduğu; yazarların ise tüm yapay zekâ destekli içeriği gözden geçirip doğruladığı, her nihai kararı verdikleri ve çalışmanın tüm sorumluluğunu üstlendikleri belirtiliyor. Yazarın da işaret ettiği gibi, bu işbölümü, modelin akıl yürütmenin büyük kısmını — çok yakın zamana kadar bir araştırma matematikçisi gerektiren argümanları doldurma ve boşlukları onarma kısmını — üstlenmiş olma ihtimalini açık bırakıyor. Yazar kanıtı tam olarak doğrulamış değil; kısmen başka bir yapay zekâ modeliyle yürütülen ilk okumada bariz bir sorun çıkmamış ve makalenin Leiden Declaration'ın yapay zekâ şeffaflığı ilkelerine uyduğu bildiriliyor.

En yüksek maruziyetli meslek

Yazı, OpenAI'nin GPT-4'ün lansmanıyla birlikte yayımladığı, çeşitli mesleklerin büyük dil modellerine ne kadar maruz kaldığını modelleyen bir teknik rapora değiniyor. Matematikçiler incelenen her kategoride zirvedeydi: işin yüzde yüzü, çalışmadaki üç emek modelinin tümünde maruz kaldığı değerlendirilmişti; bu, yazarları, çevirmenleri, sanatçıları ve grafik tasarımcıların önünde bir sıralamaydı. Yazarın okuması, matematiğin etkileri hissetmesinin sadece daha uzun sürdüğü yönünde; gecikmenin alanın doğal zorluğından çok, sınırlı eğitim verisine ve mütevazı doğrudan ekonomik değerine borçlu olduğunu öne sürüyor.

Matematik için bir konservatuvar

Denemenin merkezindeki metafor klasik müzik: toplumun konservatuvarlar aracılığıyla korumayı seçtiği bir sanat formu; az sayıda uygulayıcı eğitiliyor ve en iyilerden küçük bir gruba profesyonel olarak icra etmesi için ödeme yapılıyor. Yazara göre saf matematik zaten böyle bir kurumun — akademinin — içinde yaşıyor: üniversiteler dışında az iş var ve sonuçları küçük topluluklar anlıyor.

Ardından gelen sorular pratik. Yapay zekâ araçları uzun bir argümanın doğru olup olmadığını değerlendirmeyi zorlaştırabilir; bir makine belirleyici entelektüel emek verdiğinde itibar, fon ve tenure tahsis etmek daha da zorlaşır. Yazar, matematikçilerin ürettiği artık bilgisayarların üretebileceğiyle karşılaştırılamaz hale geldiğinde toplumun insan matematikçiler kültürünü desteklemeye devam edip etmeyeceğini sorarak bitiriyor ve edeceğini umduğunu ifade ediyor.

Neden önemli

Tek bir haftadaki iki bağımsız sinyal — matematiğin en ünlü teoremlerinden birinin tamamlanmış makine doğrulamalı formalizasyonu ve açık duran bir araştırma kestiriminin kabul edilmiş yapay zekâ destekli kanıtı — yapay zekâ sistemlerinin artık sınıf alıştırmaları değil, profesyonel matematik düzeyinde çalıştığını gösteriyor. Yapay zekâ destekli kanıtlar rutinleşirse darboğaz matematik üretmekten, onu doğrulamaya ve anlamaya kayıyor; bu da Lean gibi proof assistant'ları ve Leiden Declaration gibi şeffaflık normlarını disiplinin geleceğinin merkezine yerleştiriyor. Wang ve Wu kanıtı hâlâ topluluk tarafından tam olarak incelenmeyi bekliyor ve tek bir deneme bütün bir alanın araştırması değil; ama anlattığı kayma artık preprint'lerde de formalizasyon depolarında da görünür durumda.