22 PERKALIAN, TIDAK KURANG SATU PUN

Konflik kepentingan. Para penulis menyatakan bahwa agen AI — Claude, buatan Anthropic — menulis kode pencarian dan pembuktian Lean yang tidak memerlukan auditor manusia, di bawah arahan mereka, sementara bagian yang harus diaudit manusia dirancang oleh para penulis. Artikel ini juga ditulis oleh Claude.

Mengalikan dua kisi angka berbentuk persegi — matriks — dengan cara buku sekolah membutuhkan n³ perkalian untuk kisi dengan n baris dan n kolom. Strassen menunjukkan bahwa dua matriks 2 × 2 dapat dikalikan dengan 7 perkalian, bukan 8. Trik ini dapat diterapkan secara rekursif: potong matriks besar menjadi empat blok, perlakukan setiap blok sebagai satu angka, lalu ulangi. Biayanya kemudian tumbuh seperti n^2,807, bukan n³. Menurut makalah ini, resep 2 × 2 tersebut dibuktikan optimal pada 1971.

Gagasan yang sama berlaku untuk ukuran tetap apa pun. Resep yang mengalikan dua matriks 3 × 3 dengan r perkalian, dan tetap berlaku ketika entri-entrinya berupa blok, menghasilkan biaya yang tumbuh seperti n pangkat log₃ r. Aritmetika sederhana menunjukkan taruhannya: resep semacam itu mengalahkan Strassen tepat ketika r bernilai 21 atau kurang, dan kalah pada 22 atau lebih. Resep 3 × 3 terbaik yang dikenal, dari Laderman, memakai 23 perkalian dan belum diperbaiki sejak 1976.

Pintu yang masih sedikit terbuka

Bilangan terbaik yang mungkin untuk suatu masalah disebut rank-nya. Batas bawah rank perkalian 3 × 3 merangkak naik perlahan: 19 pada 2003, lalu 20 pada Maret 2026, dihitung oleh Wang dalam sistem bilangan mungil yang hanya berisi 0 dan 1, di mana 1 + 1 = 0. Pada September 2026, Wang dan sebuah tim yang dipimpin Yang mencapai 21 secara independen, dalam selang sepuluh hari satu sama lain. Namun 21 masih menyisakan ruang bagi resep 3 × 3 yang lebih cepat daripada milik Strassen.

Isaac Rudich, dari Polytechnique Montréal dan Carnegie Mellon University, serta Louis-Martin Rousseau, dari Polytechnique Montréal, kini telah mendorong batas itu menjadi 22.

Teorema 1. Setiap algoritma yang mengalikan dua matriks 3 × 3 dengan konstanta bilangan bulat, dan dapat diterapkan secara rekursif pada blok berukuran berapa pun, memakai sedikitnya 22 perkalian.

Jadi tidak ada algoritma semacam itu yang dapat lebih baik daripada sekitar n^2,814 — dan tidak ada yang dapat mengalahkan metode 2 × 2 Strassen.

496 teka-teki yang lebih kecil

Pembuktian ini dibangun di atas tabel rancangan Wang, yang memecah masalah sulit menjadi 496 masalah yang lebih mudah. Masing-masing menambahkan “syarat” pada matriks pertama — misalnya, bahwa entri-entri tertentu berjumlah nol. Makin banyak syarat, makin mudah masalahnya, hingga kasus remeh di mana matriks seluruhnya berisi nol.

Para penulis terlebih dahulu membangun program pencarian eksak yang memberi tahu mereka jawaban sebenarnya untuk setiap teka-teki sebelum mereka mencoba membuktikannya. Jawaban-jawaban itu berfungsi sebagai peta: menunjukkan batas bawah mana yang layak dikejar. Pada akhirnya, pembuktian mereka memberi batas bagi ke-496 teka-teki, menyelesaikan 359 di antaranya secara eksak — dibandingkan 195 dalam hasil terbaru Wang — dan menaikkan batas bawah untuk 252. Sebuah teorema “perekatan” buatan mereka sendiri menggabungkan resep untuk dua teka-teki yang lebih mudah menjadi resep untuk teka-teki ketiga, dan menyumbang 145 batas atas.

Dua syarat penting dalam pernyataan akhir. Konstanta bilangan bulat: resep dengan konstanta bilangan bulat, jika dibaca dalam sistem bilangan 0 dan 1, tetap menjadi resep yang sah tanpa tambahan perkalian, sehingga batasnya berlaku juga. Blok: tanpa syarat itu, jalan pintas memang ada. Algoritma 3 × 3 milik Rosowski, yang dikutip dalam makalah, hanya butuh 21 perkalian, tetapi bergantung pada sifat komutatif bilangan dan tidak dapat diterapkan secara rekursif.

Pembuktian yang diperiksa mesin

Pembuktian ini ditulis dalam Lean, bahasa pemrograman di mana sebuah teorema hanya berhasil dikompilasi jika setiap langkahnya terverifikasi. Pembuktian lengkapnya mencapai sekitar satu juta baris yang tersebar di 3.521 modul, dan pemeriksaannya memakan waktu 11,1 jam pada satu inti prosesor. Tidak ada yang perlu membaca semuanya. Seorang auditor membaca pustaka sekitar 1.000 baris, yang ditulis para penulis sebelum ada pembuktian apa pun, yang mendefinisikan apa itu resep perkalian dan menyatakan teoremanya; kernel Lean memeriksa sisanya, dan pemeriksa independen dapat memutar ulang hasilnya.

Para penulis juga mencatat bahwa agen AI menelusuri literatur: mereka memeriksa bahwa setiap rujukan memang ada, “tetapi tidak memeriksa bahwa setiap rujukan memuat persis gagasan yang kami atribusikan kepadanya”.

Celah terakhir

Satu pertanyaan tersisa: apakah ada resep 3 × 3 dengan 22 perkalian, atau 23 milik Laderman memang minimum sebenarnya? Para penulis memperkirakan celah itu “akan segera tertutup”, dan akan merilis kode pencarian mereka begitu hal itu terjadi, atau begitu makalah ini diterima untuk diterbitkan. Batas ini juga tidak mencakup resep dengan konstanta bukan bilangan bulat.