Dengan Busy Beaver Kelima, Para Peneliti Mendekati Batas Komputasi
(quantamagazine.org)- Busy Beaver Challenge, yang melibatkan lebih dari 20 orang dari seluruh dunia, memverifikasi bilangan Busy Beaver untuk mesin Turing 5 aturan, BB(5)=47.176.870
- Dipastikan bahwa mesin yang ditemukan Marxen dan Buntrock pada 1989, yang berhenti setelah 47.176.870 langkah, benar-benar merupakan mesin berhenti 5 aturan yang berjalan paling lama
- Tim memproses puluhan juta kandidat dengan menggabungkan metode pohon silsilah untuk mengurangi kandidat duplikat, program penentu non-berhenti, dan proof assistant Coq
- Hasil akhir diselesaikan sebagai bukti Coq 40.000 baris oleh mxdys, yang mengintegrasikan teknik komunitas, dan ditinjau oleh pakar Coq Inria, Yannick Forster
- Pada BB(6), mesin 6 aturan Antihydra, yang mirip dengan Collatz conjecture, muncul sebagai penghalang; ada kemungkinan BB(5) menjadi bilangan Busy Beaver terakhir yang diketahui manusia secara tepat
BB(5) telah dipastikan
- Tim Busy Beaver Challenge memverifikasi nilai tepat BB(5) sebagai 47.176.870
- Nilai ini berarti jumlah langkah maksimum yang dapat dijalankan oleh mesin Turing yang berhenti di antara mesin dengan 5 aturan
- Verifikasi menggunakan Coq proof assistant, dan Coq mengesahkan bahwa bukti matematis tersusun tanpa kesalahan
- Cristopher Moore dari Santa Fe Institute menilai rekayasa sosial dan matematis dalam pekerjaan ini mengesankan
- Damien Woods dari Maynooth University menyamakan kecepatan munculnya hasil ini dengan “wilayah Usain Bolt”
- Nilai konkret BB(5) terutama penting bukan karena aplikasinya di bidang ilmu komputer lain, melainkan sebagai capaian di batas ketidakmungkinan komputasi
Masalah Busy Beaver dan masalah berhenti
- Masalah Busy Beaver tidak menargetkan bahasa pemrograman umum, melainkan mesin Turing
- Mesin Turing membaca dan menulis 0 dan 1 pada pita tak hingga, sementara head bergerak satu kotak demi satu kotak sesuai tabel aturan
- Setiap aturan menentukan tindakan berikutnya berdasarkan apakah nilai yang sedang dibaca adalah 0 atau 1
- Mengubah atau mempertahankan nilai
- Bergerak ke kiri atau ke kanan
- Menentukan aturan yang akan dirujuk berikutnya
- Aturan khusus menentukan kapan mesin berhenti
- Masalah untuk menentukan secara umum apakah suatu mesin Turing pada akhirnya akan berhenti atau berjalan selamanya adalah masalah berhenti
- Alan Turing membuktikan bahwa masalah berhenti tidak memiliki solusi umum
- Perburuan Busy Beaver bukan memecahkan secara umum apakah semua mesin berhenti, melainkan mengklasifikasikan tiap mesin dalam himpunan terbatas dengan jumlah aturan tetap
Busy Beaver game dari Radó
- Dalam makalah tahun 1962, Tibor Radó mendefinisikan Busy Beaver game dengan mengelompokkan mesin Turing menurut jumlah aturannya
- Dalam himpunan semua mesin Turing dengan n aturan:
- Sebagian mesin berjalan selamanya
- Sebagian mesin berhenti
- Di antara mesin yang berhenti, mesin yang berjalan paling lama adalah busy beaver
- Jumlah langkah eksekusinya adalah BB(n)
- Untuk memastikan BB(n), perlu memeriksa waktu eksekusi semua mesin yang berhenti dan membuktikan bahwa semua mesin lainnya tidak berhenti
- Pengukuran waktu eksekusi biasanya dapat dilakukan dengan simulasi komputer, tetapi pembuktian non-berhenti mirip dengan memecahkan masalah berhenti untuk mesin tertentu
- Kontributor Busy Beaver Challenge Shawn Ligocki memandang pekerjaan ini sebagai sesuatu yang dilakukan di “batas ketidaktahuan”
Dari BB(1) hingga BB(4)
- BB(1)=1 mudah diverifikasi
- Jika aturan pertama dibuat berhenti saat membaca 0, mesin berhenti pada langkah pertama
- Selain itu, mesin terus bergerak di sepanjang pita yang terisi 0
- Dengan hanya 2 aturan saja sudah muncul lebih dari 6.000 mesin Turing berbeda; 3 aturan meningkat menjadi jutaan, dan 4 aturan menjadi miliaran
- Allen Brady mengintegrasikan metode pohon silsilah ke dalam program komputer untuk mengelompokkan mesin dengan perilaku awal yang sama dan mengurangi duplikasi
- Shen Lin bersama Radó membuktikan BB(3)=21, dan hasilnya diterbitkan pada 1965
- Brady menemukan mesin 4 aturan yang berhenti setelah 107 langkah pada 1966, lalu membuktikan pada 1974 bahwa mesin itu adalah BB(4)
- Selama lebih dari 40 tahun setelah itu, BB(4) menjadi bilangan Busy Beaver terakhir yang diketahui manusia
Perburuan Busy Beaver kelima
- Kompetisi Dortmund pada 1984 merupakan perburuan berskala besar pertama menuju BB(5)
- Mesin Turing 5 aturan berjumlah hampir 17 triliun, dan bahkan jika didaftar satu per satu setiap 1 milidetik, prosesnya akan memakan waktu lebih dari 500 tahun
- Mesin tersibuk yang ditemukan peserta Dortmund berjalan lebih dari 100.000 langkah sebelum berhenti
- Setelah itu, seorang peneliti menemukan mesin yang berjalan lebih dari 2 juta langkah
- Heiner Marxen dan Jürgen Buntrock mengembangkan teknik matematis untuk mempercepat simulasi mesin Turing
- Pada 1989, Marxen menjalankan program selama akhir pekan di komputer baru yang kuat milik perusahaannya, dan menemukan mesin yang berhenti setelah 47.176.870 langkah
- Buntrock mereproduksi hasilnya, dan keduanya menerbitkan makalah pada awal 1990
- Mesin ini sebenarnya adalah Busy Beaver kelima, tetapi diperlukan lebih dari 30 tahun lagi untuk membuktikan bahwa semua mesin yang tersisa tidak berhenti
Skelet dan mesin-mesin yang belum terpecahkan
- Pada awal 2000-an, ilmuwan komputer Bulgaria Georgi Ivanov Georgiev sangat dekat dengan BB(5)
- Georgiev menghabiskan beberapa jam setiap hari selama 2 tahun untuk memperbaiki program yang mengidentifikasi mesin non-berhenti
- Program akhirnya berupa 6.000 baris kode padat tanpa komentar, dan butuh lebih dari 1 minggu untuk dijalankan
- Program ini menyisakan sekitar 100 mesin Turing yang belum terpecahkan, lalu Georgiev menguranginya lewat analisis manual menjadi 43 mesin
- Georgiev memublikasikan hasilnya secara online pada 2003 dengan nama samaran Skelet
- Ke-43 mesin sulit ini kemudian disebut Skelet machines, mengikuti nama samarannya
- Georgiev mengatakan bahwa setelah dua tahun kerja intensif, ia begitu lelah hingga tak mampu lagi menghasilkan ide baru
Struktur kolaborasi Busy Beaver Challenge
- Tristan Stérin memulai Busy Beaver Challenge pada 2022
- Proyek ini berjalan sebagai kolaborasi online dan tumbuh menjadi komunitas internasional beranggotakan lebih dari 20 orang, termasuk banyak kontributor tanpa kredensial akademik tradisional
- Stérin menilai bahwa untuk memastikan BB(5), diperlukan bukti yang terdokumentasi dan dapat direproduksi
- Program Georgiev sangat canggih, tetapi sulit ditinjau oleh peneliti lain
- Stérin membagi pekerjaan berdasarkan pendekatan yang sudah ada
- Menghapus mesin duplikat dengan metode pohon silsilah Brady
- Mengidentifikasi mesin yang berhenti dalam 47.176.870 langkah
- Menangani mesin yang berjalan selamanya dengan program independen yang memuat metode pembuktiannya masing-masing
- Program tahap pertama yang ditulis pada akhir 2021 menghasilkan daftar sekitar 120 juta mesin Turing yang cukup untuk menentukan BB(5)
- Dari jumlah itu, sekitar seperempat berhenti sebelum mesin Marxen dan Buntrock, dan 88 juta tetap menjadi objek peninjauan
- Stérin juga membangun antarmuka online diagram ruang-waktu yang menampilkan perilaku mesin sebagai kisi dua dimensi berisi 0 dan 1
Bahasa pita tertutup dan percepatan kolaborasi
- Shawn Ligocki bergabung dengan Busy Beaver Challenge pada 2022 dan menghidupkan kembali metode bahasa pita tertutup yang dibuat Marxen
- Metode ini menyediakan kerangka matematis terpadu yang menggunakan pola pada pita mesin Turing untuk menunjukkan bahwa sebuah mesin tidak berhenti
- Ligocki menulis artikel blog yang memperkenalkan teknik tersebut, tetapi belum tahu cara menulis program yang mencakup semua kasus
- Setelah Justin Blanchard bergabung dengan proyek, ia mengimplementasikannya, dan dua kontributor lain meningkatkan kecepatan eksekusinya secara besar-besaran
- Dalam beberapa bulan, metode bahasa pita tertutup menjadi salah satu alat terkuat tim
- Teknik ini juga mampu menangani 10 dari 43 Skelet machine yang ditinggalkan Georgiev
- Ligocki menilai hasil ini tidak akan muncul dari kontribusi satu orang saja
Skelet #1, Skelet #17, dan Coq
- Skelet #1 adalah mesin yang bergantian menampilkan fase yang dapat diprediksi dan fase kacau
- Pada Maret 2023, Ligocki dan Pavel Kropitz memperkuat teknik simulasi terakselerasi berusia 30 tahun dari Marxen dan Buntrock untuk menganalisis Skelet #1
- Skelet #1 baru memasuki siklus berulang setelah melewati 1 triliun×1 triliun langkah, dan siklus berulang itu panjangnya lebih dari 8 miliar langkah
- Programmer otodidak berusia 21 tahun, mei, mempelajari Coq lalu menerjemahkan berbagai bukti Busy Beaver Challenge ke Coq
- mei juga memindahkan bukti non-berhenti Skelet #1 dari Ligocki dan Kropitz ke Coq, sehingga hasil tersebut menjadi lebih kuat
- Skelet #17 adalah mesin sulit lain yang dipecahkan dengan terobosan dari Chris Xu
- Bukti Xu sangat hebat, tetapi memuat intuisi matematis yang sulit dipindahkan ke bentuk presisi yang dituntut Coq
- Tim menginginkan bukti yang masuk akal untuk direproduksi, bukan bukti semacam “jalankan program selama 6 bulan”
Bukti Coq 40.000 baris
- Pada April 2024, kontributor baru yang hanya dikenal dengan nama samaran mxdys bergabung untuk menyelesaikan bukti Coq
- Lokasi maupun latar belakang pribadi mxdys juga tidak diketahui tim
- Pada 10 Mei, mxdys menulis di Discord, “The Coq proof of BB(5) is finished.”
- Dalam beberapa minggu, mxdys mengintegrasikan teknik dan hasil komunitas menjadi satu bukti Coq 40.000 baris
- Bukti tersebut dipublikasikan di repositori Coq-BB5
- Pakar Coq dari Inria, Yannick Forster, meninjau bukti ini dan menilai bahwa memformalkannya bukan pekerjaan mudah
- Hasilnya, mesin 47.176.870 langkah yang ditemukan Marxen dan Buntrock lebih dari 30 tahun lalu dipastikan benar-benar merupakan Busy Beaver kelima
- Georgiev menyampaikan bahwa ia tidak berharap masalah ini akan terselesaikan semasa hidupnya
- Allen Brady meninggal pada 21 April 2024 dalam usia 90 tahun, satu bulan sebelum bukti selesai
BB(6) dan batas berikutnya
- Para kontributor Busy Beaver Challenge mulai menyiapkan makalah akademik resmi yang menjelaskan hasil ini
- Makalah tersebut akan melengkapi bukti Coq mxdys dengan bukti yang dapat dibaca manusia
- Sebagian anggota tim beralih ke Busy Beaver berikutnya
- mxdys dan Racheline menemukan penghalang yang tampaknya sulit diatasi pada BB(6)
- Penghalang ini adalah mesin 6 aturan dengan masalah berhenti yang mirip dengan Collatz conjecture
- Mesin ini disebut Antihydra
- Keterkaitan antara mesin Turing dan Collatz conjecture dapat ditelusuri hingga makalah Pascal Michel tahun 1993, tetapi Antihydra tampaknya merupakan mesin terkecil yang tidak dapat dipecahkan tanpa terobosan konseptual dalam matematika
- Scott Aaronson memandang BB(5) mungkin menjadi bilangan Busy Beaver terakhir yang akan diketahui manusia
- Sebagian kontributor berencana terus mengerjakan variasi masalah Busy Beaver, tetapi tidak semua peserta tetap berada di arah yang sama
- Stérin menjadi yakin akan efektivitas cara riset kolaboratif online melalui Busy Beaver Challenge, dan ingin mengembangkan perangkat lunak untuk membantu proyek kolaboratif di bidang matematika lainnya
1 komentar
Komentar Hacker News
Ada komentar yang ditulis Scott Aaronson tentang hasil ini: https://scottaaronson.blog/?p=8088
Dan ada juga beberapa utas besar dari awal tahun ini terkait “leisure-class beavers”:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
Sebenarnya masalah busy beaver punya banyak varian, salah satunya adalah busy beaver fungsional yang didefinisikan dengan lambda calculus [1]
Karena mengukur ukuran program dalam bit, bukan jumlah state, lebih banyak nilai bisa ditentukan; sejauh ini untuk mesin Turing baru ada 6, sedangkan yang ini sudah sampai 37. Jarak antara nilai terbesar yang diketahui dan nilai yang melampaui Graham's Number juga hanya 13 bit program. Varian yang berkaitan erat [2] bisa diekspresikan langsung dengan kompleksitas Kolmogorov, dan Mikhail Andreev [3] memandang ini penting untuk aplikasi teori informasi
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
Saya menemukan https://oeis.org/A141475, tetapi di sana untuk 5 tertulis 27 triliun
Saya ingat pernah melihat video yang menjelaskan definisi itu
Saya pernah bekerja beberapa tahun dengan seorang engineer yang luar biasa dan sulit dipahami saking pintarnya, yang naik jenjang IC lebih cepat daripada siapa pun yang pernah saya lihat di perusahaan tech elite
Ia keluar beberapa tahun lalu, dan ketika saya bertanya rencananya, ia bilang akan meneliti masalah busy beaver. Saya penasaran apakah kontributor anonim mxdys yang menyelesaikan bukti formal BB(5) di artikel ini adalah orang itu, tetapi mungkin saya tidak akan pernah tahu
Saya tidak tahu imbalannya apa, dan dengan kecerdasan sehebat itu, saya berharap ia menyelesaikan masalah yang lebih relevan untuk memperbaiki dunia
Makalah busy beaver asli Tibor Radó, “On Non-Computable Functions”, sebenarnya cukup mudah dan menyenangkan untuk dibaca
Versi modern dengan anotasi tambahan ada di sini: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Hal yang menonjol di sini adalah bahwa buktinya adalah bukti Coq
Saya penasaran apakah ini bukti penting pertama yang sejak awal diimplementasikan dalam proof assistant, bukan bukti yang sudah diketahui lalu dipindahkan ke proof assistant. Sebelumnya memang sudah ada bukti berbantuan komputer, tetapi teorema empat warna atau dugaan Kepler baru kemudian dipindahkan ke lingkungan verifikasi formal
Masalah utamanya adalah decider dan bukti manualnya belum tertata dan agak meragukan. Khususnya Skelet #1 membutuhkan program khusus untuk mempercepat hingga pola akhir [0], dan Skelet #17 membuat Xu harus menggunakan penalaran padat sepanjang 7 halaman untuk membuktikan non-halting [1]. Bukti Coq keseluruhan memberi tingkat kepercayaan yang memang dibutuhkan hasil-hasil ini
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
Mungkin saya tidak memahami persis apa yang dimaksud dengan “lingkungan verifikasi formal”, tetapi setahu saya teorema empat warna memang dibuktikan dengan komputer sejak awal. Upaya pembuktian awal Kempe punya cacat, tetapi menyediakan sebagian alat dasar yang dipakai dalam pembuktian berikutnya, dan pada akhirnya teorema itu tampaknya dibuktikan dengan komputer
Busy beaver ini ditemukan pada 1990, dan semua mesin berukuran 5 kemungkinan juga dienumerasi tak lama setelah itu
Selamat kepada tim. Dengan ini, masalah penghentian untuk program mesin Turing 5-status 2-simbol pada pita kosong bisa dibilang telah terpecahkan
Saya penasaran apakah ada yang sudah mencoba menerapkan teknik yang sama pada kasus 2-status 4-simbol. Secara umum, simbol memang lebih kuat daripada status, tetapi pada skala itu sepertinya masih mungkin ditangani dan bisa saja menghasilkan hasil yang tak terduga. 6-status 2-simbol dan 2-status 5-simbol sama-sama tampak sulit ditangani, dan mungkin bahkan bisa dibuktikan sulit. Selain itu, ada gagasan konyol tetapi anehnya tersebar luas bahwa manusia bisa mengintuisi jawaban masalah penghentian lewat mata batin atau mekanika kuantum di otak; tentu saja, hal seperti itu tidak terlibat dalam pembuktian ini
Setahu saya, decider yang dipakai saat ini saja sudah cukup untuk membuktikan bahwa semua kasus tersisa pada 2×4 tidak berhenti. Jadi jika tidak ada kesalahan besar dalam desain decider, dari juara saat ini diperoleh Σ(2,4) = 2.050, S(2,4) = 3.932.964. Hanya saja hasilnya belum dirangkum di satu tempat
Pada 2×5 ada Hydra dan pada 6×2 ada Antihydra; keduanya menghitung iterasi yang sama, hanya berbeda pada titik awal dan kondisi berhenti. Dugaan standarnya, terkait masalah 3/2 Mahler, adalah bahwa iterasi ini berdistribusi merata modulo 2; jika dugaan itu dibuktikan, kita bisa memperoleh batas atas dan bawah untuk rasio kumulatif 0 dan 1, sehingga hampir pasti dapat membuktikan bahwa kedua mesin tersebut tidak berhenti. Tentu saja belum ada metode pembuktian yang diketahui
Mereka menggunakan pembangkit bukti berbasis teori logika bernama Aleph*, dan saat itu sudah diketahui sejak 1.500 tahun sebelumnya bahwa ZFC tidak dapat menetapkan BB(18). Dibandingkan dengan tahun 2024, program apa pun yang ada jauh sebelum Aleph* digunakan bahkan secara teoretis pun tidak bisa dipakai untuk pemeriksaan bukti brute force guna menyelesaikan BB(18). Ini berbeda dengan hari ini, ketika kita secara teoretis bisa menyelesaikan BB(??) dengan mengenumerasi dan memeriksa bukti ZFC
Posisi “manusia mengintuisi jawaban masalah penghentian” maksudnya seperti ini. Sejauh yang saya tahu, tidak ada alasan teoretis kuat yang membuat sejarah masa depan semacam itu mustahil. Dan karena busy beaver tidak dapat dihitung, manusia harus mengembangkan teori baru untuk membuat program yang dibutuhkan. Kredit atas hasil itu harus diberikan kepada sesuatu, dan karena program tersebut belum ada saat itu, kreditnya tidak bisa diberikan kepada komputasi
Saya penasaran apakah semua program panjang 5 yang tidak berhenti kebetulan semuanya dapat dibuktikan tidak berhenti
“Fakta bahwa Σ(5) = 1.915 dan S(5) = 2.358.064 tidak akan pernah dibuktikan. Atau jika batas bawah yang lebih besar ditemukan, nilai baru itu bisa dimasukkan ke prediksi ini.”
Alasannya adalah besar kemungkinan alam telah menyisipkan setidaknya satu masalah di antara mesin 5-status yang tertunda yang sama sulit ditangkapnya dengan dugaan Goldbach. Dengan kata lain, ada kemungkinan besar terdapat pola rekursif tidak berhenti yang melampaui kemampuan kita untuk mengenalinya. Untungnya prediksi ini tidak menjadi kenyataan, tetapi selisihnya hanya satu status tambahan
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", dalam Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, hlm. 259–277. Bab ini juga dapat ditemukan dalam edisi ke-2, Springer, 1995, hlm. 237–254.
Jika dalam arti praktis, orang lain sudah menjawabnya. Jika dalam arti matematis, akan cukup mengejutkan jika BB(5) ternyata tidak dapat diputuskan. Sebab 5-status 2-simbol terlalu kecil untuk mengodekan perilaku yang tidak dapat diputuskan
Namun sebagai konsekuensi dari teorema ketaklengkapan, pasti ada suatu n yang nilainya untuk BB(n) tidak dapat dibuktikan oleh matematika standar. Dalam beberapa tahun terakhir, sejumlah orang meneliti seberapa rendah n semacam itu bisa diturunkan, dan rekor saat ini[0] adalah 745. Rekor ini mungkin bisa diturunkan lagi, tetapi tetap saja ada jarak besar antara nilai tertinggi yang kita ketahui, 5, dan nilai terendah yang kita tahu tidak dapat diketahui, 745
[0] Jika penasaran apa yang dimaksud “matematika standar”, ini adalah rekor saat ini untuk ZFC maupun PA. Jadi setidaknya untuk PA, sepertinya penurunan lebih lanjut seharusnya mungkin. Sejauh ini tampaknya belum ditemukan cara yang lebih baik untuk PA daripada untuk ZFC, tetapi bukankah seharusnya itu mungkin?
“Baru empat hari sebelumnya, kontributor lain bernama mxdys dan Racheline menemukan penghalang untuk BB(6) yang tampaknya sulit dilampaui. Itu adalah mesin 6-aturan yang masalah penghentiannya menyerupai dugaan Collatz, masalah matematika yang terkenal sulit ditangani. Koneksi antara mesin Turing dan dugaan Collatz dapat ditelusuri kembali ke makalah tahun 1993 oleh matematikawan Pascal Michel, tetapi mesin yang baru ditemukan bernama ‘Antihydra’ tampaknya merupakan mesin terkecil yang tidak dapat diselesaikan tanpa terobosan konseptual dalam matematika.”
Saya pernah menulis program sebagai proyek pribadi untuk memecahkan masalah cutting stock (https://en.wikipedia.org/wiki/Cutting_stock_problem)
Stoknya mencakup pemotongan potongan berbentuk /---/, /---|, |---|, dan karena saya tidak ingin membuang material pada potongan 45 derajat, saya tidak bisa atau tidak ingin memakai program yang sudah ada. Penjelasan bahwa Brady memangkas subtree pencarian yang perbedaannya tidak penting untuk mengoptimalkan pencarian BB(4) terasa menarik, karena cukup mirip dengan hal yang saya lakukan saat membuat program saya cepat
Menurut tulisan blog Scott Aaronson, ada 16.679.880.978.201 mesin Turing 5-status
Saya penasaran apakah diketahui berapa persen di antaranya yang berhenti. Sunting: jumlah mesin Turing n-status adalah (4n + 1)^(2n). Saya menemukan data untuk n kecil yang mirip dengan analisis yang saya cari: https://github.com/LukasKalbertodt/beaver
Saya tidak menemukannya di situs bbchallenge.org, tetapi semua mesin sudah diklasifikasikan
Secara keseluruhan, pembuktiannya tergolong cukup singkat. Termasuk spasi dan komentar, jumlahnya 19.000 baris Coq
Berdasarkan pengalaman saya, jika dikompilasi menjadi makalah tradisional, kemungkinan akan jauh lebih pendek daripada versi Coq. Tentu saja panjang pembuktian bukan ukuran tingkat kesulitan atau kompleksitas, tetapi bisa dipakai sebagai tolok ukur yang sangat kasar
Saat membicarakan batas pengetahuan manusia, kita sering membayangkan teorema-teorema yang sebenarnya dapat dibuktikan, tetapi terlalu kompleks untuk dipahami manusia mana pun. Barangkali pembuktian paling kompleks yang kita miliki adalah klasifikasi grup sederhana hingga, yang mencapai ribuan hingga puluhan ribu halaman, dan kemungkinan hanya sedikit sekali orang di dunia—atau bahkan tidak ada—yang memahaminya sepenuhnya
Seperti disebutkan dalam artikel, BB(6) mungkin saja tak dapat diputuskan. Namun ada juga kemungkinan bahwa ia memiliki pembuktian berjuta-juta halaman sehingga berada di luar jangkauan umat manusia