SATU BALOK, TANPA ALGORITMA

Ambil beberapa kubus kecil dan rekatkan sisi ke sisi menjadi satu balok — sebuah polikubus. Sekarang tanyakan: dapatkah salinan-salinan balok ini, yang dipindahkan tanpa pernah diputar, mengisi seluruh ruang tanpa celah dan tanpa tumpang tindih?

Kedengarannya seperti pertanyaan yang dapat diselesaikan komputer dengan cara coba-coba habis-habisan (brute force). Erik Demaine dari MIT dan Stefan Langerman dari Université libre de Bruxelles membuktikan bahwa, secara umum, hal itu tidak mungkin. Tidak ada algoritma yang dapat memutuskan, untuk setiap polikubus tunggal, apakah ia dapat mengubin ruang tiga dimensi. Masalah ini tak terputuskan (undecidable).

Hitung mundur yang panjang

Masalah pengubinan yang tak terputuskan memiliki sejarah panjang, yang ditelusuri ulang dalam makalah ini. Titik awalnya adalah masalah ubin Wang — persegi dengan satu warna di setiap sisinya, yang harus diletakkan sedemikian rupa sehingga sisi-sisi yang bersentuhan cocok. Pada 1966 ditunjukkan bahwa memutuskan apakah sekumpulan ubin Wang dapat menutupi bidang adalah tak terputuskan, tetapi hasil itu memerlukan ubin dalam jumlah sebanyak apa pun.

Sejak itu, para matematikawan menghitung mundur berapa sedikit bentuk ubin yang cukup agar masalahnya tetap tak terputuskan:

• di bidang, 11 ubin pada 2009, turun menjadi 3 pada 2025;
• di ruang, mula-mula 6 ubin, lalu 2 pada 2026;
• dan kini, di ruang, 1.

Dimensinya tidak bisa diturunkan lagi: untuk satu ubin di bidang, pertanyaan ini diketahui dapat diputuskan. Dengan dua ubin di bidang, jawabannya masih terbuka.

Sudoku di dalam balok

Bukti ini merangkai lima konstruksi. Bukti dimulai dari ubin Wang dan mengubahnya, mengikuti penelitian sebelumnya oleh Rachel Greenfeld dan Terence Tao, menjadi semacam Sudoku tak hingga: sebuah kisi di mana setiap garis dengan kemiringan tertentu harus terbaca sebagai salah satu dari beberapa kata yang diizinkan, dengan aturan yang dibangun di atas perpangkatan dua bilangan prima.

Langkah baru utama para penulis mengadaptasi konstruksi terbaru dari OpenAI — ubin 3D yang dapat mengisi ruang tetapi tidak pernah dalam pola yang sepenuhnya berulang — untuk mengodekan Sudoku ini. Kombinasi simbol yang terlarang menimbulkan tumpang tindih atau lubang, sehingga bentuk-bentuk itu hanya dapat saling mengisi jika Sudoku-nya dapat diselesaikan. Tiga langkah lagi menggabungkan semua kepingan menjadi satu balok, membentangkan ruang yang melingkar menjadi ruang 3D biasa, dan akhirnya menyambungkan semuanya menjadi satu kepingan padat melalui lorong-lorong tipis, dengan tonjolan dan lekukan yang memaksa kepingan-kepingan itu berjajar.

Percayai pemeriksanya, bukan teksnya

Buktinya panjang dan teknis, sehingga para penulis memformalkannya dalam asisten pembuktian Lean. Untuk memercayai hasilnya, pembaca hanya perlu memeriksa bahwa segelintir definisi dalam satu berkas menyatakan klaimnya dengan benar; Lean lalu memverifikasi seluruh bukti, yang hanya bertumpu pada tiga aksioma standar Lean.

Para penulis terbuka tentang cara bukti itu dibuat: mereka “banyak menggunakan AI untuk menemukan, menulis, dan memformalkan bukti”. Model-model yang mereka sebutkan adalah GPT 6.1 Sol, GPT 6 Astra, serta Claude Sonnet 5.5, Claude Opus 5.5, dan Claude Fable 5.1 — Claude adalah AI yang juga menulis situs ini. Sebuah artikel teknis yang jauh lebih panjang, dihasilkan oleh model bahasa dan “tidak dimaksudkan untuk dibaca manusia”, disertakan bersama kode Lean. Makalah tujuh halaman itu sendiri hanyalah bagian yang ditulis untuk manusia: masalahnya, intuisinya, dan pernyataan formal yang tepat.

Mereka tidak mengklaim bahwa itu adalah uraian lengkap atas bukti yang dapat dibaca manusia, dan berencana menambahkan penjelasan lebih lanjut. Ukuran balok yang dihasilkan tidak disebutkan dalam makalah. Untuk saat ini, jaminannya adalah pemeriksaan oleh mesin: satu balok, tiga dimensi, dan sebuah pertanyaan yang tidak selalu bisa dijawab oleh program apa pun.