On yıldan fazla bir süredir matematikçiler 500 sayfalık bir kanıtın gerçekten doğru olup olmadığı konusunda anlaşamadılar. Artık kanıtın bilgisayarda okunabilir bir forma çevrilmesi sorunu nihayet çözebilir
Bilgisayarlar matematiksel kanıtları doğrulayabilir
Matematikteki en tartışmalı tartışmalardan biri, bilgisayar yardımıyla çözülebilir ve on yıldan uzun süredir devam eden karmaşık bir kanıt hakkındaki sert tartışmaya potansiyel olarak son verilebilir.
Sorun, 2012 yılında, Japonya’daki Kyoto Üniversitesi’nden Shinichi Mochizuki’nin, sayıların tam kalbinden vuran çözülmemiş önemli bir problem olan ABC varsayımı için 500 sayfalık geniş bir kanıtla matematik dünyasını şaşkına çevirmesiyle başladı. Kanıt, Mochizuki tarafından icat edilen, evrensel Teichmüller (IUT) teorisi adı verilen ve onu anlamaya çalışan çoğu uzman matematikçi için bile aşılmaz görünen son derece teknik ve anlaşılması güç bir çerçeveyi kullanıyordu.
Şu anda 40 yıldan daha eski olan ABC varsayımı, üç tam sayının (a + b = c) görünüşte basit bir denklemini içerir ve bu sayıları oluşturan asal sayıların birbirleriyle nasıl ilişki kurması gerektiğini belirler. Toplama ve çarpmanın nasıl etkileşime girdiğinin temel doğasına ilişkin derin bilgiler vermenin yanı sıra bu varsayım, Fermat’nın Son Teoremi gibi diğer ünlü matematiksel varsayımlar için de çıkarımlar içerir.
Bu potansiyel sonuçlar, matematikçileri başlangıçta kanıtı doğrulama konusunda hevesli hale getirdi, ancak ilk çabalar boşa çıktı ve Mochizuki, çalışmayı sindirmek için daha fazla çaba gösterilmediğinden yakındı. Daha sonra 2018’de iki önde gelen Alman matematikçi, Bonn Üniversitesi’nden Peter Scholze ve Frankfurt Goethe Üniversitesi’nden Jakob Stix, kanıtın zırhında olası bir çatlak bulduklarını duyurdular.
Ancak Mochizuki onların iddiasını reddetti ve kimin haklı ya da haksız olduğuna karar verecek büyük bir yargı organı olmadığından, IUT teorisinin geçerliliği iki kampta dondu: bir tarafta matematik camiasının çoğu; diğer yanda Mochizuki’ye ve onun profesör olduğu Kyoto’daki Matematik Bilimleri Araştırma Enstitüsü’ne gevşek bağlı olan küçük bir araştırmacı grubu.
Şimdi Mochizuki çıkmaza olası bir çözüm önerdi. Kanıtın, insanlar için tasarlanmış matematiksel gösterimdeki mevcut formundan, bir bilgisayar tarafından otomatik olarak kontrol edilip doğrulanabilen, Yalın adı verilen bir programlama diline çevrilmesini önerdi.
Biçimselleştirme adı verilen bu süreç, matematiğin yapılma şeklini tamamen değiştirebilecek, devam eden bir araştırma alanıdır. Mochizuki’nin kanıtının resmileştirilmesi daha önce önerilmişti, ancak bu, projede ilerleme arzusunu ilk kez belirtti.
Mochizuki, bu makale için yorum talebine yanıt vermedi, ancak yakın tarihli bir raporunda, Lean’ın, matematikçiler arasında, kendi kanıtının geniş çapta kabul edilmesini engelleyen türdeki anlaşmazlıkları çözmek için çok uygun olacağını savundu: “(Yalın), matematiksel gerçeği sosyal ve politik dinamiklerin boyunduruğundan kurtarma temel hedefi açısından anlamlı ilerleme elde etmek için en iyi ve belki de tek teknolojidir” diye yazıyor Mochizuki.
Mochizuki’ye göre, Temmuz ayında Tokyo’da Yalın üzerine yakın zamanda düzenlenen bir konferansa katıldıktan sonra, özellikle de onun IUT teorisi için gerekli olduğunu söylediği matematiksel yapı türlerini idare etme yeteneğini gördükten sonra, resmileştirmenin yararları konusunda ikna olmuştu.
Imperial College London’dan Kevin Buzzard, bu çıkmazın aşılmasına yardımcı olmak için potansiyel olarak umut verici bir yön olduğunu söylüyor. “Eğer Yalın’da yazılıyorsa, bu çılgınca değil, değil mi? Gazetelerdeki pek çok şey çok garip bir dilde yazılıyor, ancak bunları Yalın’da yazabiliyorsanız, o zaman bu, en azından bu garip dilin tamamen iyi tanımlanmış bir şey haline geldiği anlamına gelir” diyor.
Hollanda’daki Utrecht Üniversitesi’nden Johan Commelin, “(IUT’nin) nedenini anlamak istiyoruz ve bunu 10 yıldan fazla bir süredir bekliyorduk” diyor. “Lean bu cevapları anlamamıza yardımcı olabilir.”
Ancak hem Buzzard hem de Commelin, IUT teorisini resmileştirmenin devasa bir girişim olacağını ve şu anda yalnızca insan tarafından okunabilir biçimde var olan tonlarca matematiksel denklemin çevrilmesini gerektireceğini söylüyor. Bu proje, genellikle uzman matematikçilerden ve Yalın programcılardan oluşan ekiplerin dahil olduğu, aylar veya yıllar süren, şimdiye kadar tamamlanmış en büyük resmileştirme çalışmalarından bazılarıyla aynı düzeyde olacaktır.
Bu göz korkutucu olasılık, projeyi üstlenmeye hak kazanan az sayıdaki matematikçi için çekici olmayan bir teklif olabilir. Buzzard, “İnsanlar, zamanlarının çoğunu, sonuçta başarısızlığa dönüşebilecek bir proje üzerinde çalışmaya harcamak isteyip istemedikleri konusunda büyük bir karar vermek zorunda kalacaklar” diyor.
Ancak matematikçiler projeyi tamamlamayı başarsalar ve Yalın kod, Mochizuki teoreminin hiçbir çelişkisi olmadığını gösterse bile, Commelin, Mochizuki’nin kendisi de dahil olmak üzere matematikçilerin hala bunun anlamı üzerinde kavga edebileceğini söylüyor.
“Yalın çok fazla etkiye sahip olabilir ve tartışmalara son verebilir, ancak yalnızca Mochizuki işini resmileştirmek için yeni kararına gerçekten sadık kalırsa” diyor. “Dört ay sonra çekip giderse ve ‘Tamam, bunu denedim ama Lean benim kanıtımı anlayamayacak kadar aptal’ derse, o zaman bu, hala sosyal bir soruna takılıp kaldığımız çok uzun bir dizi bölümden oluşan yeni bir bölümdür.”
Ve Mochizuki’nin Yalın’a karşı gösterdiği tüm iyimserliğe rağmen, aynı zamanda kodun anlamını yorumlamanın daha fazla anlaşmazlığa yol açabileceği konusunda eleştirmenleriyle aynı fikirde ve Yalın’ın “şu anda sosyal ve politik sorunların tam çözümü için herhangi bir tür ‘sihirli tedavi’ oluşturacak gibi görünmediğini” yazıyor.
Ancak Buzzard, başarılı bir resmileştirmenin, özellikle de Mochizuki başarılı olursa, en azından on yıllık destanı devam ettirebileceğinden umutlu. “Yazılımla tartışamazsınız” diyor.
