Yapay zeka, yirmi yıllık matematik problemini çözdü

Macar matematikçi Paul Erdős'ün geride bıraktığı 1109 matematik problemi arasında yer alan ve yirmi yıldır çözülemeyen Problem 367, son zamanlarda yapay zeka teknolojisinin desteğiyle kanıtlanabildi. Bu başarı, matematikte bilgisayar teknolojisinin ve yapay zekanın kullanımının giderek normalleştiğini göstermektedir. Ünlü matematikçi Terence Tao, bu önemli gelişmeyi sosyal medya platformu Mastodon'da paylaşarak, yapay zekanın matematik alanındaki rolünün artık tartışılmaz olduğunu vurgulamıştır.

Erdős'ün Mirasından Çıkan Çözüm

Paul Erdős, sadece geçen yüzyılın en önemli matematikçilerinden biri değil, aynı zamanda yaşam tarzı ve kişiliğiyle de dikkat çeken bir figürdür. Sabit bir ikametgahı olmadan bir bavulla yaşayan, enstitüden enstitüye seyahat eden Erdős, matematiksel çalışmalarıyla tanınmakla birlikte, Holokost'ta ailesinin büyük bölümünü kaybetmiş acılı bir geçmişe sahiptir. 'Yeni bir çatı, yeni bir kanıt' mottosuyla bilinen matematikçi, 1996'daki ölümüne kadar Leonhard Euler'in yanında tüm zamanların en üretken matematikçisi olarak kabul edilmiştir. Erdős'ün kaleminden çıkan bu muazzam sayıdaki problem ve varsayım, günümüzde hala matematikçilerin ilgisini çekmektedir.

İngiliz Manchester Üniversitesi'nden matematikçi Thomas Bloom, Erdős'ün tüm problemlerini derleyerek ayrı bir web sitesine aktarmıştır. Bu sitede yer alan 1109 problem arasında, asal sayılarla ilgili olan Problem 367, uzun yıllar boyunca çözülmemiş durumda kalmıştır. Hollandalı amatör matematikçi Wouter van Doorn, bu problemin bir bölümünü çürüttüğüne inandığını web sitesinde bildirmiş, ancak kanıtını tamamlamak için yardım arayışına girmiştir.

Yapay Zekanın Rolü ve Başarısı

Terence Tao, Wouter van Doorn'un çalışmasında eksik olan detayları fark ederek, Google'ın Deep Think yapay zeka sistemine danışmaya karar vermiştir. Bu sistem, oldukça karmaşık bir kanıt sunmuş olsa da, Tao tarafından elle basitleştirilebilmiş ve doğruluğu teyit edilmiştir. Böylece Problem 367 ilk kez çözülmüş olmuştur. Tao, çözümün daha önce yayınlanmamış olduğundan emin olmak için, yine yapay zeka desteğiyle mevcut bilimsel literatürü gözden geçirmiştir.

Ancak bu başarı, Tao'nun merakını tam olarak gidermemiştir. Matematikçi, Problem 367'nin bilgisayarlar tarafından daha resmi bir biçimde kanıtlanabileceğini düşünerek, Lean programlama dilini kullanmaya karar vermiştir. Lean, matematiğe özelleştirilmiş bir yapay zeka aracı olan Aristotle'ın yardımıyla, insan dilinde yazılmış problem formülasyonu başarıyla bilgisayar diline çevrilmiştir. Bu çeviri işlemi, bilgisayarın problemi ayrıntılı mantıksal adımlarda ele alabilmesini sağlamıştır. Dil modellerinin aksine, bilgisayar bu sayede her bir adımı açık ve anlaşılır biçimde işleyebilmiştir.