Bilgisayar Destekli Matematik İspatı: Detaylar Açığa Çıktı!

2012 yılında Japonya'nın Kyoto Üniversitesi'nden Shinichi Mochizuki, sayı teorisi alanındaki ünlü bir fikir olan ABC varsayımının kanıtını sundu. 500 sayfalık bir kanıt yayınladı. Varsayım, çözümlerinde a + b = c denklemini sağlayan sayıların nasıl ilişkili olduğunu inceleyen, asal sayılarla ilgilidir. Ancak, bu sayıların nasıl birbiriyle etkileştiği konusundaki anlayışa dair derin bilgiler gerektirir.

Mochizuki'nin kanıtı matematik camiasında bir bomba etkisi yarattı, ancak yeni teknikler ve kavramlar kullandığı için, bunlara "İnter-evrensel Teichmüller teorisi" (IUT) adını verdiği için birçok meslektaşının anlayabilmesi zor oldu. Önde gelen matematikçiler, Mochizuki ile görüşmeler de dahil olmak üzere, çalışmasını aydınlatmaya çalıştılar. Ancak, kanıtın doğruluğu konusunda bir uzlaşıya varılamadı.

2018 yılında, Almanya'daki Bonn Üniversitesi'nden Peter Scholze ve Goethe Üniversitesi Frankfurt'tan Jakob Stix, kanıtın olası bir hatasını belirlediğini açıkladılar. Mochizuki ve Kyoto Üniversitesi'ndeki yakın çalışma arkadaşları kanıtın doğru olduğunu savundu, ancak matematik camiasının daha geniş bir kesimi, kanıtın en iyi ihtimalle çözülemez ve en kötü ihtimalle ölümcül bir kusur içerdiğini savundu.

Geçen yıl, Mochizuki, muhaliflerine bir zeytin dalı uzattı ve ilerlemenin bir yolunu gösterdi. Matematiksel kanıtları bilgisayar diline çevirerek doğruluğunu otomatik olarak doğrulamak için, "formalizasyon" alanında büyük bir ilerleme kaydedilmişti. Mochizuki, bu alanda kullanılan bir dil olan Lean'i en çok beğendi. Mochizuki, "[Lean] matematiksel gerçeği sosyal ve politik dinamiklerden kurtarmak için en iyi ve belki de tek teknoloji... " dedi.

Şimdi, ABC varsayımının kanıtının Lean'de resmi olarak yürütüldüğü iki ayrı matematik grubu tarafından yürütülen çalışmalar resmi olarak başlatıldı. Mochizuki'nin de başında bulunduğu bir grup ve iki yıldan uzun süredir gizlice devam eden ancak bir engelleyen bir grup. 2023'ün sonunda, Japonya'daki ZEN Matematik Merkezi'nde Fumiharu Kato, LANA Projesi'ni başlattı. Mochizuki'nin çalışmasıyla aşina olan ve Lean'de büyük matematiksel projeleri resmi olarak gerçekleştiren uzmanları da dahil olmak üzere, Mochizuki'nin çalışmasına tanıdık matematikçiler işe aldı. Ana hedef, "tartışmayı kesin bir şekilde sona erdirmekti", dedi. Kanada'daki Alberta Üniversitesi'nden Adam Topaz, Fumiharu'nun işe aldığı kişilerden biri.