12 yıllık matematik bilmecesi yapay zekâ ile çözüldü
Yapay zeka 12 yıllık matematik bilmecesini çözdü ve bilim dünyasında taşlar yerinden oynadı. Pekin Üniversitesi bünyesindeki AI4Math ekibi, Amerikalı matematikçi Dan Anderson tarafından 2014 yılında ortaya atılan ve bugüne dek hiçbir insanın çözemediği bir varsayımı, tamamen otonom çalışan bir sistemle yaklaşık 80 saat içinde çürüttü. Daha da çarpıcı olan şu: Sistem sadece cevabı bulmakla kalmadı, bulduğu ispatı Lean 4 adlı formel doğrulama dilinde satır satır kanıtlayarak mühürledi.
12 Yıldır Raflarda Bekleyen Problem Neydi?
Dan Anderson, 2014 yılında değişmeli cebir alanında “yarı-tam Noether yerel halkaları” ile ilgili bir önerme ortaya atmıştı. Anderson, Iowa Üniversitesi’nde uzun yıllar görev yapmış ve 2022’de 73 yaşında hayatını kaybetmiş saygın bir cebircidir. Ortaya koyduğu varsayım, Riemann Hipotezi gibi milyon dolarlık ödüller vaat eden dev problemler kadar popüler değildi. Ancak tam da bu yüzden ilginç bir sınav niteliğindeydi: Ne çok kolaydı ne de imkansız derecede karmaşık. Tam 12 yıl boyunca matematikçilerin kafasını kurcaladı ama kimse elini taşın altına koyup kesin bir sonuca varamadı.
İki Beyinli Sistem: Rethlas ve Archon Nasıl Çalışıyor?
Ekibin geliştirdiği mimari, tek bir yapay zekanın değil, birbiriyle konuşan iki ayrı ajanın ürünü. İlk ajanın adı Rethlas. Bu sistem, tıpkı bir matematikçinin kütüphanede kaynak taraması yapması gibi, Matlas adlı devasa bir teorem arama motorunda geziniyor. Matlas’ın içinde on milyonlarca matematiksel ifade ve kanıtlanmış önerme var. Rethlas bu dağınık bilgi yığınının içinden, Anderson’ın varsayımını çürütebilecek kritik bir bağlantıyı bulup çıkardı: “tam halka tamlaması” adı verilen ve ilk bakışta konuyla alakasız görünen bir teori. Bu teoriyi kullanarak bir karşı örnek inşa etti.
Sıra ikinci ajandaydı: Archon. Rethlas’ın doğal dille yazdığı bu ispat taslağını alıp LeanSearch motoruyla Lean 4 diline çevirdi. Lean 4, her adımın mantıksal olarak kusursuz olmasını zorlayan etkileşimli bir teorem kanıtlama sistemi. Archon işi daha da ileri götürdü: Çeviri sırasında Rethlas’ın ilk planında gizli bir mantık boşluğu keşfetti. Hiçbir insan müdahalesi olmadan stratejiyi baştan aşağı yeniden kurguladı. Hatta ihtiyaç duyduğu bazı matematiksel kavramlar Lean 4’ün kütüphanesinde yoktu; Archon bu durumda da pes etmedi, alternatif tanımlar üzerinden dolambaçsız bir yol bularak ispatı tamamladı. Ortaya çıkan sonuç, yaklaşık 19 bin satırlık, her virgülüne kadar makine tarafından onaylanmış dev bir Lean 4 kodu oldu.
“İnsan Elinden Çıkmış Gibi Değil” Kaygısına Son
Yapay zeka modellerinin en büyük handikabı, “halüsinasyon” denen uydurma eğilimidir. Özellikle matematik gibi mutlak kesinlik isteyen bir alanda, tek bir mantık hatası tüm ispatı çöpe çevirir. Bu sistemin asıl çığır açan yanı, Rethlas’ın ürettiği fikirleri Archon’un Lean 4 süzgecinden geçirerek bu riski sıfıra indirgemesi. Araştırmacılar makalelerinde “İnsan operatörden hiçbir matematiksel yargı talep edilmedi” ifadesini kullandı. İnsanın tek yaptığı, sistemin erişemediği kısıtlı bazı dosyaları indirip sunucuya yüklemekten ibaretti.
Hız Faktörü: Deneyimli Bir Uzmandan 10 Kat Daha Verimli
Çalışmanın belki de en çarpıcı teknik detayı hız. Ekip, Archon’un bu ölçekte bir formel doğrulamayı, Lean 4 konusunda deneyimli bir insan uzmandan en az on kat daha hızlı tamamladığını raporladı. Üstelik sistem, ispat sürecinde altı farklı harici akademik makalenin kritik sonuçlarını da koda başarıyla entegre etti. Normalde aylar sürecek bir süreç, makineler arasındaki bu sessiz diyalog sayesinde birkaç güne sığdırıldı. Araştırmacılar, bir insan matematikçinin Archon’a sadece hafifçe rehberlik etmesi halinde sürenin çok daha da kısalabileceğini not düşüyor.
Bilim Dünyası Ne Diyor?
Çalışma henüz hakem değerlendirmesinden geçmiş değil; bulgular 4 Nisan 2026’da arXiv ön baskı sunucusunda yayımlandı. Bu nedenle akademik çevreler temkinli bir iyimserlik içinde. Çin Bilimler Akademisi üyesi ve ünlü matematikçi Tian Gang, bu başarının AI ile matematiğin derin entegrasyonu için yeni bir paradigma sunduğunu belirtti. Pekin Üniversitesi Matematik Bilimleri Fakültesi Dekanı Liu Ruochuan ise meselenin sadece bir problemi çözmek olmadığını, gelecekte matematikçilerin iş yapış biçimini kökten değiştirecek bir yöntemin doğrulandığını vurguladı.
Sırada Ne Var?
Anderson varsayımının çözümü, yapay zekanın artık sadece veri sınıflandıran veya metin üreten bir araç olmaktan çıkıp, otonom bir araştırmacıya dönüştüğünün en somut kanıtı. Gelecekte makinelerin kendi başlarına hangi zorlu teorilerin üstesinden geleceği merak konusu. Belki de çok yakında, bir yapay zekanın Fields Madalyası’na aday gösterildiğini konuşuyor olacağız. hedefbilgitoplumu.com
