24 günde 15.000 sayfa matematik: Yapay zekâ ajanları “devasa teoremi” denetledi
Axiom girişimi, sonlu basit grupların sınıflandırma kanıtını yapay zekâ ajanı sürüleriyle Lean'de tümüyle biçimselleştirdiğini açıkladı. Kanıt henüz bağımsız olarak yeniden oluşturulmadı.
Grafik: TERRA WORLD NEWS (belirtilen kaynaklara dayalı kendi grafiğimiz)
Sonlu basit grupların sınıflandırması, matematiğin en uzun kanıtı olarak kabul ediliyor: yaklaşık 100 matematikçinin onlarca yıl boyunca yazdığı 500'den fazla makalede yaklaşık 15.000 sayfa. Axiom Math girişimi, bilgisayarın her mantıksal adımı denetlediği Lean kanıt doğrulayıcısının diline tüm kanıtı aktardığını duyurdu. Bunun için onlarca yapay zekâ ajanı sürüler hâlinde 24 gün çalıştı; ortaya yaklaşık 43,1 milyon satır Lean kodu çıktı.
Axiom'a göre ajanlar, yayımlanmış literatürde 34 kayda değer sapma buldu; bunlardan önemli olanları insan matematikçiler inceledi. Axiom, grup kuramcıları Richard Lyons ve Ronald Solomon'dan danışmanlık aldı. İnsanlar ayrıca biçimsel ifadelerin gerçekten kastedilen teoremi ifade edip etmediğini kontrol etti. “Devasa teorem” terimini bir zamanlar matematikçi Daniel Gorenstein ortaya atmıştı.
Bunun bilgisayarla tümüyle doğrulanmış ilk kanıt olduğu, şimdilik yalnızca Axiom'un kendi beyanı. Şirket dışında kimsenin kanıtı yeniden oluşturup denetleyip denetlemediği sorulduğunda, şirketin CEO'su Carina Hong, RuntimeWire'a göre “Henüz değil” yanıtını verdi. Hong'un aktardığına göre Axiom, dış grupları buna teşvik etmek için derleme dosyalarını yayımlıyor.