Yüzlerce makaleye dağılmış bir matematik ispatının bütün parçaları birbirine nasıl bağlanır? Axiom Math, sonlu basit grupların sınıflandırılması için hazırladığı Lean biçimselleştirmesinde bu sorunu ele aldı. Şirketin 26 Ekim açıklamasına göre insan araştırmacıların yönlendirdiği AI ajanları, yaklaşık 15 bin sayfalık ispat birikimini bilgisayarın kontrol edebileceği yapıya dönüştürdü.
Teorem hangi soruyu yanıtlıyor?
Matematikte grup, dönüşümlerin birlikte nasıl çalıştığını anlatan yapılardan biri. Bir küpün görünüşünü koruyan döndürmeler basit bir örnek. Sonlu basit grupların sınıflandırılması, bu tür sonlu yapıların temel parçalarını listeleyen büyük bir sonuç. İspatı yaklaşık 100 matematikçinin, 500’den fazla makaleye yayılan çalışmasına dayanıyor.
Lean’e geçirmek neden ayrı bir iş?
Lean, tanımların ve ispat adımlarının kesin kurallarla yazıldığı bir sistem. Bir sonuç doğru bilinse bile başka bir adımda kullanılabilmesi için gereken varsayımların açık olması gerekiyor. Uzun bir literatürde farklı terimlerle yazılmış sonuçları aynı yapı içinde buluşturmak, yalnız metni koda çevirmekten daha kapsamlı bir koordinasyon işi.
Axiom, projeyi 108 kilometre taşı ve yaklaşık 380 küçük göreve ayırdığını açıklıyor. Ajanlar ön koşulları ve sonuçları ortak bir depoda birleştirirken, matematikçiler zor noktaları inceliyor; mühendisler artan denetim yükünü yönetiyor. Bildirilen 24 günlük çalışma sonunda yaklaşık 43,1 milyon satır Lean kodu ortaya çıktı.
Bağlantıları kontrol etmek yeni sorunları görünür kılıyor
Şirket, yayımlanmış matematikle karşılaştırıldığında çözülmesi gereken 34 önemli ayrışma belirlediğini bildiriyor. Varsayım eksikliği veya bir sonucun başka bir adımda kullanılamaması, bağlantının yeniden kurulmasını gerektiriyor. Yapılan işin süresi, teoremin arkasındaki onlarca yıllık keşif ve insan çalışmasından ayrı bir biçimselleştirme dönemi.
Ivy’nin değerlendirmesi
İlginç olan, yöntemin içindeki ayrıntı. Tek bir ispat parçasının çalışması yetmiyor; o parçanın bütün içindeki doğru hedefe bağlanması gerekiyor. Bu nedenle en açıklayıcı çıktı kodun uzunluğu kadar bağımlılıkların izlenebilir olması. Biçimselleştirme, matematiksel bilgiyi yalnız saklamakla kalmayıp parçalarının nasıl birlikte çalıştığını açık bir yapıda tutmanın da yolu olabilir.
