22 ÇARPMA, BİR EKSİĞİ BİLE OLMAZ

Çıkar çatışması. Yazarlar, arama kodunu ve bir insan denetçiye ihtiyaç duymayan Lean kanıtlarını kendi yönlendirmeleri altında yapay zekâ ajanlarının — Anthropic’in Claude’u — yazdığını, bir insanın denetlemesi gereken kısmı ise kendilerinin tasarladığını belirtiyor. Bu makale de Claude tarafından yazılmıştır.

İki kare sayı tablosunu — matrisleri — okulda öğretilen yolla çarpmak, n satır ve n sütunluk tablolar için n³ çarpma gerektirir. Strassen, iki 2 × 2 matrisin 8 yerine 7 çarpmayla çarpılabileceğini gösterdi. Hile özyinelemeli olarak uygulanabilir: büyük bir matrisi dört bloğa bölün, her bloğu tek bir sayı gibi ele alın ve tekrarlayın. Maliyet bu durumda n³ yerine n^2,807 gibi büyür. Makaleye göre bu 2 × 2 tarifin optimal olduğu 1971’de kanıtlandı.

Aynı fikir her sabit boyut için işe yarar. İki 3 × 3 matrisi r çarpmayla çarpan ve girdiler blok olduğunda da çalışan bir tarif, n üzeri log₃ r gibi büyüyen bir maliyet verir. Basit bir aritmetik neyin söz konusu olduğunu ortaya koyuyor: böyle bir tarif Strassen’i tam olarak r 21 ya da daha az olduğunda geçer, 22 ve üzerinde geride kalır. Bilinen en iyi 3 × 3 tarif, Laderman’ınki, 23 çarpma kullanıyor ve 1976’dan beri iyileştirilemedi.

Aralık kalmış bir kapı

Belirli bir problem için mümkün olan en iyi sayıya onun rankı (rank) denir. 3 × 3 çarpmanın rankı için alt sınırlar yavaş yavaş yükseldi: 2003’te 19, ardından Mart 2026’da 20 — bunu Wang, yalnızca 0 ve 1’den oluşan ve 1 + 1 = 0 olan minik bir sayı sisteminde hesapladı. Eylül 2026’da Wang ve Yang liderliğindeki bir ekip, birbirinden bağımsız olarak, on gün arayla 21’e ulaştı. Ama 21 hâlâ Strassen’inkinden hızlı bir 3 × 3 tarife yer bırakıyordu.

Polytechnique Montréal ve Carnegie Mellon Üniversitesi’nden Isaac Rudich ile Polytechnique Montréal’den Louis-Martin Rousseau sınırı şimdi 22’ye çıkardı.

Teorem 1. İki 3 × 3 matrisi tam sayı sabitlerle çarpan ve her boyuttaki bloklara özyinelemeli olarak uygulanabilen her algoritma en az 22 çarpma kullanır.

Dolayısıyla böyle hiçbir algoritma yaklaşık n^2,814’ten daha iyisini yapamaz — ve hiçbiri Strassen’in 2 × 2 yöntemini geçemez.

496 küçük bulmaca

Kanıt, zor problemi 496 daha kolay probleme bölen ve Wang tarafından geliştirilen bir tabloya dayanıyor. Her biri birinci matrise “koşullar” ekliyor — örneğin bazı girdilerinin toplamının sıfır olması. Koşullar arttıkça problem kolaylaşıyor; en sonunda matrisin tamamen sıfır olduğu önemsiz duruma varılıyor.

Yazarlar önce, her bulmacanın gerçek cevabını onu kanıtlamaya çalışmadan önce söyleyen kesin bir arama programı geliştirdi. Bu cevaplar bir harita işlevi gördü: hangi alt sınırların peşine düşmeye değer olduğunu gösterdi. Sonunda kanıtları 496 bulmacanın tümüne sınır koyuyor, 359’unu kesin olarak çözüyor — Wang’ın son sonuçlarındaki 195’e karşı — ve 252’sinin alt sınırını yükseltiyor. Kendilerine ait bir “yapıştırma” (gluing) teoremi, iki kolay bulmacanın tariflerini üçüncü bir bulmacanın tarifinde birleştiriyor ve üst sınırların 145’ini sağladı.

Son ifadede iki koşul önemli. Tam sayı sabitler: tam sayı sabitli bir tarif, 0 ve 1 sayı sisteminde okunduğunda daha fazla çarpma gerektirmeyen geçerli bir tarif olarak kalır; böylece sınır aktarılır. Bloklar: bu şart olmadan kestirmeler mevcut. Makalede atıf yapılan Rosowski’nin 3 × 3 algoritması yalnızca 21 çarpma gerektiriyor ama sayıların değişmeli (commuting) olmasına dayanıyor ve özyinelemeli olarak uygulanamıyor.

Bir makinenin denetlediği kanıt

Kanıt, bir teoremin ancak her adımı doğrulandığında derlendiği bir programlama dili olan Lean’de yazılmış. Kanıtın tamamı 3.521 modüle dağılmış yaklaşık bir milyon satır tutuyor ve tek bir işlemci çekirdeğinde denetlenmesi 11,1 saat sürüyor. Kimsenin hepsini okuması gerekmiyor. Bir denetçi, yazarların henüz hiçbir kanıt yokken yazdığı, bir çarpma tarifinin ne olduğunu tanımlayan ve teoremi ifade eden yaklaşık 1.000 satırlık bir kütüphaneyi okuyor; geri kalanını Lean’in çekirdeği denetliyor ve bağımsız bir denetleyici sonucu yeniden çalıştırabiliyor.

Yazarlar ayrıca yapay zekâ ajanlarının literatürü taradığını belirtiyor: her kaynağın var olduğunu denetlediler, “ama her birinin tam olarak ona atfettiğimiz fikri içerdiğini değil.”

Son boşluk

Bir soru kalıyor: 22 çarpmalı bir 3 × 3 tarif var mı, yoksa Laderman’ın 23’ü gerçek minimum mu? Yazarlar boşluğun “çok yakında kapanmasını” bekliyor ve arama kodlarını, boşluk kapandığında ya da makale yayına kabul edildiğinde yayımlayacaklar. Sınır ayrıca tam sayı olmayan sabitli tarifleri de dışarıda bırakıyor.